frama-c wp插件无法验证手册中的交换功能

Question

如何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键人体工程学(事实上,没有cvc3,gappa,simplify,verit,yices,z3)无法丢弃任何这些证据4和义务？

我使用最新的OPAM安装:

• frama-c:Sodium-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)

Answer 1

你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等.