In "standard" Verifiable-C, memory references cannot occur in expressions except at top level within a load statement: x = a[e]; or x = *(e.field); (same as x = e->field;) where e is any expression that does not access memory. Or, a store statement, a[e1] = e2; or e1->field = e2;...

First, the precondition '(array_at tint sh arr 0 100) (eval_id _arr) is actually present behind abbreviate in Delta hypothesis. Second, it turned out, that entailer!. tactic is not safe, and can produce unprovable goals from eligible ones. In this case, first I need to supply additional condition is_int v...

FIRST: When writing VST/Verifiable-C questions, please indicate which version of VST you are using. It appears you are using 1.4. SECOND: I am not sure this answers all your questions, but, "closed_wrt_vars S P" says that the lifted assertion P is closed with respect to all the variables in the...

My solution: define notation for WITH with 10 variables: Notation "'WITH' x1 : t1 , x2 : t2 , x3 : t3 , x4 : t4 , x5 : t5 , x6 : t6 , x7 : t7 , x8 : t8 , x9 : t9 , x10 : t10...

First: offhand, without attempting to reproduce this myself-- is it possible that using entailer! is too "risky", because (as documented) entailer! can sometimes turn a provable goal into an unprovable one. Try with entailer without the bang, and see if it looks better. Second, TT |-- emp is not true....

Yes, you are right; it should be sigma-prime.

The problem is in the argument list specification. It must contain only function arguments (no locals) It must have arguments in the same order as in the C function prototype. BTW, the order of function in Gprog must be the same as the order of function definitions in the c-file....

Your guess_sqrt_spec has an error in line 68 of verif_sqrt.v, where you give the return type as "tint" (signed integer) where the sqrt.c program has "tuint" (unsigned integer). Then the VST's forward_call tactic has a misleading and unhelpful error message, complaining about the witness type instead of the return-type mismatch....