Что мне делать, когда возникает эта ошибка? 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и (скандий)

      [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)