当出现此错误时，我该怎么办？Alt-Ergo：“未知错误”

Question

当我运行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)

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

Answer 1

你有哪个frama-c版本？

使用Alt-Ergo 2.3.3和frama-c 21.1 (Scandium)

[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.0和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)