0

我试图了解 VST 如何处理（可寻址）局部变量，所以我编写了这个函数：

int main() {
    int x = 5, y = 7;
    int *a = &x;
    int *b = &y;

    *a = 8;
    *b = 9;

    return x;
}

然后我尝试使用以下规范对其进行验证：

Definition main_spec :=
 DECLARE _main
  WITH p : int (* still toying with things, couldn't figure out how to drop this *)
  PRE [ ]
   PROP ()
   LOCAL ()
   SEP ()
  POST [ tint ]
   EX i : Z,
   PROP ( i = 8 )
   LOCAL (temp ret_temp  (Vint (Int.repr i)))
   SEP ().

一切都很顺利，只需使用 ( forward) 直到我留下来证明以下内容的 return 语句

data_at Tsh tint (vint 9) v_y * data_at Tsh tint (vint 8) v_x |-- FF

这似乎应该是无法证明的（请注意，我刚刚申请forward到这一点）。我期待一些规范说明在局部变量被释放后堆是空的，即emp |-- emp。

有什么地方可以让我获得更多关于这方面的信息吗？

谢谢！

附加信息：我挖掘了FF后置条件的来源，它来自typecheck_expr，特别是以下情况Evar：

  | Evar id ty =>
      match access_mode ty with
      | By_reference =>
          match get_var_type Delta id with
          | Some ty' =>
              tc_bool (eqb_type ty ty')
                (mismatch_context_type ty ty')
          | None =>
              tc_FF
                (var_not_in_tycontext Delta id)
          end
      | _ => tc_FF (deref_byvalue ty) (* ?? *)
      end

除非我读错了，否则这似乎表明您不能按值访问局部变量。这只是一个疏忽吗？或者语义中有什么东西可以防止这种情况发生？

4

2 回答 2

0

您使用的是哪个版本的 VST？在最近的主分支版本（commit 506f8e7）中，以下简单的证明可以正常工作。

Lemma body_main: semax_body Vprog Gprog f_main 
main_spec.
Proof.
start_function.
forward.
forward.
forward.
forward.
forward.
forward.
forward.
forward.
Exists 8.
entailer!.
Qed.
于 2018-09-24T16:15:49.937 回答
0

此失败的原因是您忘记了-normalizeclightgen 的标志。如果您使用而不是翻译.c文件，它应该可以正常工作。clightgen -normalizeclightgen

于 2018-09-25T02:27:42.553 回答