3

如何frama-c -wp验证wp 手册中的示例- 一个简单的swap函数 (swap.c)：

/* @ requires \valid(a) && \valid(b);
   @ ensures A: *a == \old(*b);
   @ ensures B: *b == \old(*a);
   @ assigns *a,*b;
   @*/
void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

调用

$ frama-c -wp -wp-rte swap.c

给出：

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function swap
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_4 : Unknown (174ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_2 : Unknown (160ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (154ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Unknown (220ms)
[wp] Proved goals:    0 / 4
     Alt-Ergo:        0  (unknown: 4)

我想知道为什么

  1. 我的尝试与手册中的目标数量不同（4 对 9）？
  2. Alt-Ergo（事实上，没有一个cvc3, gappa, simplify, verit, yices, z3）不能放弃这 4 个证明义务中的任何一个？

我使用最新的 OPAM 安装：

  • frama-c: 钠-20150201
  • alt-ergo：0.95.2（来自 ubuntu 14.04 主存储库包alt-ergo）
  • why3: 0.86.1

一个证明义务的例子，传递alt-ergo给wp：

goal swap_assert_rte_mem_access:
  forall t : int farray.
  forall a_1,a : addr.
  linked(t) ->
  (region(a.base) <= 0) ->
  (region(a_1.base) <= 0) ->
  valid_rd(t, a, 1)
4

1 回答 1

5

当您swap从 WP 手册中复制规范时，您犯了一个错误。（下一个版本将使用允许复制粘贴的字体。）C 注释的开头和@ACSL 规范中的 之间不能有空格；否则注释被解释为简单注释。因此，您实际上是在尝试证明

void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

这当然是不可能的，因为a并且b可能不是有效的指针。

正确的规格是

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == \old(*b);
  @ ensures B: *b == \old(*a);
  @ assigns *a,*b;
  @*/
void swap(int * a, int * b);

在小示例中使用 Frama-C 时，您可能应该使用 GUI 界面 ( frama-c-gui)。这样，您将看到规范化后的源代码，添加了哪些 RTE 等。

于 2015-09-04T18:28:58.523 回答