1

当我运行 WP 示例时，出现错误，我不知道它是什么。

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

这是 frama-c-gui 控制台中的错误

[wp] No updated script.
[wp] [Alt-Ergo 2.3.1] Goal typed_swap_ensures_A : Failed
  Unknown error

执行“frama-c -wp -wp-rte swap.c”后的输出

[kernel] Parsing swap.c (with preprocessing)
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_assert_rte_mem_access : Failed
  Unknown error
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_ensures_A : Failed
  Unknown error
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_assert_rte_mem_access_3 : Failed
  Unknown error
[wp] Proved goals:    5 / 8
  Qed:               5  (16ms)
  Alt-Ergo 2.0.0:    0  (failed: 3)

如果你能帮助我，非常感谢

4

1 回答 1

0

你有哪个frama-c版本？

和Alt-Ergo 2.3.3（frama-c 21.1钪）

[bash] frama-c -wp -wp-rte ex.c
[kernel] Parsing ex.c (with preprocessing)
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] Proved goals:    8 / 8
  Qed:               5  (1ms-3ms-6ms)
  Alt-Ergo 2.3.3:    3  (8ms-12ms) (50)

使用Alt-Ergo 2.0.0and frama-c 21.1，我得到一个错误，但它与你的不同：

frama-c -wp -wp-rte ex.c
[kernel] Parsing ex.c (with preprocessing)
[rte] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.3.3] Goal typed_swap_assert_rte_mem_access : Failed
  Failure : File generation error :  syntax error
[wp] [Alt-Ergo 2.3.3] Goal typed_swap_ensures_A : Failed
  Failure : File generation error :  syntax error
[wp] [Alt-Ergo 2.3.3] Goal typed_swap_assert_rte_mem_access_3 : Failed
  Failure : File generation error :  syntax error
[wp] Proved goals:    5 / 8
  Qed:               5  (1ms-2ms-5ms)
  Alt-Ergo 2.3.3:    0  (failed: 3)
于 2020-12-13T19:03:07.647 回答