I try to verify my program with VST. I've got a weird error message:
Coq < Check ( (sh, n, guess-1, vn, Vint (Int.sub (Int.repr guess) (Int.repr 1)))).
> (sh, n, guess - 1, vn, Vint (Int.sub (Int.repr guess) (Int.repr 1)))
> : share * Z * Z * val * val
For me it seems like the function signature, that I'm going to use to forward_call is exactly what is reqired here (share * Z * Z * val * val)
Coq < forward_call (sh,n,guess-1,vn,Vint (Int.sub (Int.repr guess) (Int.repr 1))).
> Toplevel input, characters 0-75:
> Error: Tactic failure: Use forward_call W, where W is a witness of type
> (share * Z * Z * val * val)%type
> (level 1).
But VST complains. Where should I look? What is different here ?
BTW, if it's useful, my intermediate proof state: 1 focused subgoals (unfocused: 1-0-0) , subgoal 1 (ID 4026)
Espec : OracleKind
sh : share
n : Z
guess : Z
vn : val
vguess : val
H : repr n vn
H0 : repr guess vguess
A0 : 0 <= n
AM : n < Int.modulus
B0 : 0 <= guess
BM : guess * guess < Int.modulus
Struct_env := abbreviate : type_id_env.type_id_env
narg : name _n
guessarg : name _guess
Delta := abbreviate : tycontext
POSTCONDITION := abbreviate : ret_assert
============================
semax Delta
(PROP (repr guess vguess /\ guess > 0)
LOCAL
(`(typed_false
(typeof
(Ebinop Ole
(Ebinop Omul (Etempvar _guess tuint)
(Etempvar _guess tuint) tuint)
(Etempvar _n tuint) tint)))
(eval_expr
(Ebinop Ole
(Ebinop Omul (Etempvar _guess tuint)
(Etempvar _guess tuint) tuint) (Etempvar _n tuint) tint));
`(eq vguess) (eval_id _guess); `(eq vn) (eval_id _n))
SEP())
(Ssequence
(Scall (Some 38%positive)
(Evar _guess_sqrt
(Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint cc_default))
[Etempvar _n tuint;
Ebinop Osub (Etempvar _guess tuint) (Econst_int (Int.repr 1) tint)
tuint]) (Sreturn (Some (Etempvar 38%positive tuint))))
(overridePost (PROP () LOCAL () SEP()) POSTCONDITION)
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.