frama-c wp插件无法验证手册中的交换函数。

Question

如何使frama-c -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 -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(事实上，cvc3，gappa，simplify，verit，yices，z3)都不能放弃这4种证明义务中的任何一种？

我使用最新的OPAM安装：

• frama-c：钠-20150201
• alt-ergo：0.95.2 (来自ubuntu14.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)

Answer 1

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

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时，您可能应该使用GUI界面(frama-c-gui)。这样，您将看到您的源代码后，正常化，什么RTE已经添加，等等。