0

我尝试用 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)
4

1 回答 1

2

您的guess_sqrt_spec 在verif_sqrt.v 的第68 行有一个错误，您将返回类型指定为“tint”（有符号整数），而sqrt.c 程序有“tuint”（无符号整数）。

然后 VST 的 forward_call 策略有一个误导和无益的错误消息，抱怨见证类型而不是返回类型不匹配。

于 2014-12-15T13:50:48.610 回答