It seems that tc_expr is constrained to knowledge of the typing context and nothing else so it is not possible to safely "typecheck" an expression that requires knowledge of the heap state, e.g. a pointer dereference as the condition of a while loop. Why is that and would it ever be possible for me to prove correct a loop such as:
char *t = ...;
...
while (*t != 0)
{
...
t++;
}
I would think while loops could optionally be proven with a variation of tc_expr that does allow for pointer dereference by accounting for the heap context along with the typing context. I suspect that the thinking is that a loop condition should be a “pure” expression, but I’m ultimately curious if that is really a necessary constraint.
P.S. I realize that I could rewrite this as a for loop. My question still stands knowing that VST allows me to prove this kind of loop albeit with different syntax.
Answer number 1: It's a design decision, one way or the other, and we found that many things are simpler (and more in the spirit of Separation Logic) if expressions do not access memory.
Answer number 2: You can write this while loop, just as it is. Then use clightgen with the -normalize flag (which you should always use anyway), and then you can verify it. However, in such a case, the loop form will not be (strictly speaking) a Clight "while" loop, it will have it's loop-test (if (?) then /*skip*/; else break;) in the middle of the loop body; so you will use forward_loop to prove it, instead of forward_while.