Regarding the return type of \sizeof_object() (or, more importantly, the type for the second argument of, for example, \thread_local_array()), I would actually much rather have it be \natural at the top-level, with a refinement and appropriate range checks hidden in the Boogie model.

This may make error-reporting a bit icky, but it avoids a lot of explicit casting in annotations, when you write your spec using spec integers and try to use those variables in function contracts. In the best case, it means that you can truly see your spec as a language-independent mathematical description of the problem and its solution, and the contract as simply stating "the code computes this mathematical function I just described (or it doesn't terminate)". In the worst case, you still have a fairly clear description of your problem in terms of mathematical integers, even if you do go ahead and lay them out inside language-specific constructs such as structures and other unions.

Again, maybe it's just a matter of my verification philosophy and style not matching the VCC spirit, in which case you can ignore my remark (I don't want to start a debate here, although I did go on a bit of a rant). In any case, my problem can also be fixed by automatically inserting checked casts from spec integer types to real integer types wherever they are needed. Casts in the other direction are (I believe) already automatically inserted.

You misunderstand, I'm not proposing to make the argument types to functions (like \thread_local_array()) more restrictive, just the return types of functions (like \sizeof_object()). This makes the contracts of these functions stronger (whereas strengthening the argument types makes them weaker). This should not introduce additional casting burden, because they are automatically cast up to integer in annotations anyway. If anything, it would save you casting (e.g., inside an _(unchecked) subexpression).

Sorry for the misunderstanding: I saw "stricter types" and the mention of naturals and bad memories surfaced.

Maybe the work item could also include weakening integer argument types where possible (I'm mostly thinking of the array predicates, but I'm sure there are more)?