我正在使用VST 2.5和Coq 8.11.0
使用非标准的调用约定对函数执行forward_call
时出错。最小的代码示例:
struct t {
int t_1;
int t_2;
};
struct t test_aux() {
struct t ret;
ret.t_1 = 1;
ret.t_2 = 2;
return ret;
}
void test_f() {
test_aux();
}
VST规格:
Require Import VST.floyd.proofauto.
Require Import example.
Definition Vprog : varspecs. mk_varspecs prog. Defined. Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Open Scope Z.
Definition aux_spec : ident * funspec := DECLARE _test_aux
WITH res : val
PRE [tptr (Tstruct _t noattr)]
PROP ()
PARAMS (res)
GLOBALS ()
SEP (data_at_ Tsh (Tstruct _t noattr) res)
POST [tvoid]
PROP ()
LOCAL ()
SEP (data_at Tsh (Tstruct _t noattr)
(Vint (Int.repr 1), Vint (Int.repr 2)) res).
Definition test_spec : ident * funspec := DECLARE _test_f
WITH temp : val
PRE []
PROP ()
PARAMS ()
GLOBALS ()
SEP (data_at_ Tsh (Tstruct _t noattr) temp)
POST [tvoid]
PROP ()
LOCAL ()
SEP ().
Definition Gprog := ltac:(with_library prog [aux_spec; test_spec]).
Theorem test : semax_body Vprog Gprog f_test_f test_spec. Proof. start_function. Fail forward_call (nullval). Admitted.
错误:
Unable to unify "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
tvoid cc_default" with "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
tvoid
{|
cc_vararg := false;
cc_unproto := false;
cc_structret := true |}".
我不知道这是错误还是预期的行为,所以我在这里有几个问题:
1)这是错误吗?
2)如果没有,存在什么变通办法来证明这种情况?
[遗憾的是,VST不支持结构复制,结构传递或结构返回。另请参阅this question。因此,如果不更改该程序,就无法验证它。