I got a question, about VST support for compcert built-in annotation mechanism. Suppose we have a C function:
int f(int *p) {
// p is not null
__builtin_annot("_p <> nullval");
int t = *p;
return t;
}
And specification for it:
Definition f_spec : ident * funspec :=
DECLARE _f
WITH p_b : block, p_ofs : ptrofs, a : Z
PRE [(tptr tint)]
PROP ()
PARAMS (Vptr p_b p_ofs)
GLOBALS ()
SEP (data_at Tsh (tptr tint) (Vint (Int.repr a)) (Vptr p_b p_ofs))
POST [tint]
PROP ()
LOCAL (temp ret_temp (Vint (Int.repr a)))
SEP (data_at Tsh (tptr tint) (Vint (Int.repr a)) (Vptr p_b p_ofs)).
When I'm trying to prove this, I got to the state, where I have this statement (builtin EF_annot 1 "_p <> nullval" []([]);
to prove next and I can't move forward from here.
hint tactic doesn't help, forward and it's variations(if, loop, etc) doesn't work either.
So the question is, how(if i can) I move forward from here?
