Тактическая ошибка: используйте формулу forward_call W.

Question

Я пытаюсь проверить свою программу с помощью VST. У меня странное сообщение об ошибке:

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 

Для меня это кажется как функция подписи, что я собираюсь использовать для forward_call именно то, что здесь (обязательными для заполнения 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). 

Но VST жалуется. Где я должен смотреть? Что здесь другое?

Кстати, если это полезно, мое промежуточное состояние доказательства: 1 сосредоточены подзадачи (нецеленаправленная: 1-0-0) , подцель 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) 

Answer 1

Вашего guess_sqrt_spec имеет ошибку в строке 68 of verif_sqrt.v, , где вы указываете тип возврата как «tint» (целое число со знаком), где программа sqrt.c имеет «tuint» (целое число без знака).

Тогда тактика команды VST forward_call вводит в заблуждение и unhelpful сообщение об ошибке, жалуясь на тип свидетеля вместо несоответствия возвращаемого типа.