gpt4 book ai didi

c - VST forward_call 在非标准调用约定上失败

转载 作者:行者123 更新时间:2023-12-04 10:10:45 25 4
gpt4 key购买 nike

我使用的是 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)如果不是,有什么解决方法可以证明这种情况?

更新:

在使用以下解决结构复制限制的解决方法后,我们遇到了这个问题:我们定义了一个 struct_normalize : statement -> statement Coq 中的函数,用逐字段赋值替换结构赋值。因此,我们假设我们正在调用的函数中没有结构体复制。也就是说,我们可以验证 test_aux从上面的例子。所以问题是:
  • 是否forward_call失败只是因为 cc_structret := truetest_aux AST?
  • 鉴于我们规范了函数并从函数体中删除了结构复制,更改 structret 是否安全?相应的值(value)并继续进行证明?
  • 最佳答案

    不幸的是,VST 不支持结构复制、结构传递或结构返回。另见 this question .所以你不能在不改变它的情况下验证这个程序。

    关于c - VST forward_call 在非标准调用约定上失败,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/61351513/

    25 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com