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行目にエラーがあります.sqrt.cプログラムには「tuint」（符号なし整数）がありますが、戻り値の型を「tint」（符号付き整数）として指定します。

次に、VST の forward_call タクティックには、戻り値の型の不一致ではなく、witness の型について不平を言う、誤解を招く役に立たないエラー メッセージがあります。

于 2014-12-15T13:50:48.610 に答える