0
VST로 프로그램을 확인하려고합니다. 내가 forward_call에 사용 거라는 것은 여기 전술적 실패 : forward_call W. 메소드 서명을 사용하십시오.
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).
(share * Z * Z * val * val)
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
는 함수 서명처럼 보인다 : 나는 이상한 오류 메시지가 있어요 그러나 VST는 불평합니다. 어디를 봐야합니까? 여기 다른 점은 무엇입니까? 유용의 경우
BTW, 내 중간 증거 상태 : 1 집중 하위 목표 (초점이 맞지 : 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)