Блог

Главная - Вопросы по программированию - Что мне делать при возникновении этой ошибки? Alt-Ergo: «Неизвестная ошибка»

Что мне делать при возникновении этой ошибки? Alt-Ergo: «Неизвестная ошибка»

#frama-c #alt-ergo

#frama-c #alt-ergo

Вопрос:

Когда я запускаю пример WP, появляется ошибка, и я не знаю, что это такое.

 /*@ requires valid(a) amp;amp; 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)

Большое вам спасибо, если вы можете мне помочь

Комментарии:

1. Я получаю эти точные ошибки для одного и того же файла. Вы когда-нибудь выясняли, в чем проблема?

Ответ №1:

Какая версия frama-c у вас есть?

С Alt-Ergo 2.3.3 помощью and 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 помощью and 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)

Комментарии:

1. Вы обновляли конфигурацию Why3 между двумя испытаниями? (Frama-C 21: rm ~/.why3.conf ; why3 config --full-config , Frama-C 22: rm ~/.why3.conf ; why3 config --detect ).

2. Когда я использую команду:** why3 config —detect**, результат докажет, что версия 2.3.3 Alt-Ergo, как известно, не поддерживается. Известные версии для этой проверки: 2.3.1, 2.3.0. Известные старые версии для этой проверки: . добавлена 1 проверка (ы) (включая 1 проверку (ы) с нераспознанной версией) Сохраните конфигурацию в /home/charles/.why3.conf . Итак, моя версия Alt-Ergo 2.3.0

3. И какую версию Frama-C вы используете?

4. Версия Frama-C — 21.1

5. С Frama-C 21.1 вы должны сделать: rm ~/.why3.conf ; why3 config --full-config . (И для Frama-C 22 , rm ~/.why3.conf ; why3 config --detect ). Обратите внимание, что тот факт, что проверка не поддерживается Why3, не обязательно означает, что она не будет работать, просто она еще не была протестирована.