Тактическая ошибка: используйте 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

Ваш угадайзник_спекта содержит ошибку в строке 68 файла verify_sqrt.v, в которой тип возвращаемого значения указан как "tint" (целое число со знаком), а в программе sqrt.c "tuint" (целое число без знака).

Затем в тактике VST forward_call появляется ошибочное и бесполезное сообщение об ошибке с жалобой на тип свидетеля, а не на несоответствие типа возврата.