0

这次我证明函数调用其他。vars.c：

int pure0 ()
{
    return 0;
}

int get0(int* arr)
{
    int z = pure0();
    return 0;
}

我的证明开始 - verif_vars.v：

Require Import floyd.proofauto.
Require Import vars.

Local Open Scope logic.
Local Open Scope Z.

Definition get0_spec :=
  DECLARE _get0
    WITH sh : share, arr : Z->val, varr : val
    PRE [_arr OF (tptr tint)]
        PROP ()
        LOCAL (`(eq varr) (eval_id _arr);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr 0 100) (eval_id _arr))
    POST [tint] `(array_at tint sh arr 0 100 varr).

Definition pure0_spec :=
  DECLARE _pure0
    WITH sh : share
    PRE []
        PROP ()
        LOCAL ()
        SEP ()
    POST [tint] local(`(eq (Vint (Int.repr 0))) retval).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get0_spec :: pure0_spec ::nil.

Lemma body_pure0: semax_body Vprog Gprog f_pure0 pure0_spec.
Proof.
  start_function.
  forward.
Qed.


Lemma body_get0: semax_body Vprog Gprog f_get0 get0_spec.
Proof.
  start_function.
  name arrarg _arr.
  forward_call (sh).
  entailer!.

这导致了目标：

2 subgoals, subgoal 1 (ID 566)

  Espec : OracleKind
  sh : share
  arr : Z -> val
  varr : val
  Delta := abbreviate : tycontext
  POSTCONDITION := abbreviate : ret_assert
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  arrarg : name _arr
  ============================
   Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

subgoal 2 (ID 567) is:
 DO_THE_after_call_TACTIC_NOW

我想它说明了函数调用不会改变arr内容，这对我来说很明显。

我能用这个目标做什么？哪种策略适用于此，该声明的确切含义是什么？我是否应该丰富pure0规范以某种方式指出它不会修改任何内容？

4

3 回答 3

1

FIRST：在写 VST/Verifiable-C 问题时，请注明您使用的是哪个版本的 VST。看来您使用的是 1.4。

第二：我不确定这是否能回答你所有的问题，但是，

“closed_wrt_vars S P”表示提升的断言 P 对于集合 S 中的所有变量都是封闭的。也就是说，S 是一组 C 语言标识符，可以代表不可寻址的局部变量（“temps”，而不是“vars ”）。P 是“environ->mpred”形式的断言，“close”意味着如果您将“environ”更改为对集合 S 中的任何变量具有不同的值，那么 P 的真值将不会改变。

"Forall" 是 Coq 的标准库谓词，用于将谓词应用于列表。所以，

 Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

意思是，让集合 S 是只包含变量 _z' 的单例集合。我们在这里断言列表中的所有谓词都是封闭的 S。列表中只有一个谓词，并且它是“平凡提升的”，即对于任何谓词（P：mpred），提升的谓词

`(P)

相当于 (fun rho:environ => P)。那么，“P 不关心你对 rho 做了什么，包括改变 _z 的值”。

“auto with closed”（或者只是为了确定，“auto 50 with closed”）应该解决这个问题，并且您指出它确实会解决这个问题。所以我假设你剩下的问题是，“这里发生了什么？”，我希望我能回答。

于 2015-01-18T17:27:16.177 回答
0

顺便说一句（与您的问题无关）， `isptr (eval_id _arr)get0 的先决条件可能是不必要的。已经暗示了`(array_at tint sh arr 0 100) (eval_id _arr))。

此外，假设您确实需要`isptr (eval_id _arr)先决条件；你可以考虑把它写成，

   PROP (isptr varr)
   LOCAL (`(eq varr) (eval_id _arr))
   SEP (`(array_at tint sh arr 0 100 varr))

这（在某些方面）更简单，更“规范”。

于 2015-01-18T17:34:01.327 回答
0

解决方案，用于vst/progs/verif_reverse.v：

auto with closed.

不幸的是，它只回答了一半的问题。

于 2015-01-18T15:05:32.313 回答