Пример Frama- C acsl max из руководства не работает - PullRequest
Новая
       27

Пример Frama- C acsl max из руководства не работает

0 голосов
/ 07 мая 2020

Я считаю, что мне не хватает чего-то очевидного, но я много пробовал, и мне не удалось найти источник проблемы.

Я следую acsl guide from Фрама- C. Вот вводный пример того, как проверить правильность нахождения максимального значения в массиве: 

/*@ requires n > 0;
    requires \valid(p+ (0 .. n-1));
    ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i];
    ensures \exists int e; 0 <= e <= n-1 && \result == p[e];
*/
int max_seq(int* p, int n) {
  int res = *p;
  for(int i = 0; i < n; i++) {
    if (res < *p) { res = *p; }
    p++;
  }
  return res;
}

Однако, запустив frama-c -wp -wp-prover alt-ergo samenum.c -then -report, я получаю: 

[wp] Warning: Missing RTE guards
[wp] samenum.c:8: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_seq_ensures_2 : Timeout (Qed:1ms) (10s)
[wp] [Alt-Ergo] Goal typed_max_seq_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals:    0 / 2
  Alt-Ergo:        0  (interrupted: 2)
[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'max_seq'
--------------------------------------------------------------------------------

[    -    ] Post-condition (file samenum.c, line 3)
            tried with Wp.typed.
[    -    ] Post-condition (file samenum.c, line 4)
            tried with Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.

Кажется, что alt-er go тайм-аут до подтверждения свойства. Что бы ни стоило, я попробовал с большим таймаутом, но он все равно не работает.

Я использую:

  • frama- c: 19.1
  • why3: 1.2.0
  • alt-er go: 2.3.2

Я запускаю это на Ubuntu 18.04 и перед запуском команды, которую я запускаю: why3 config --detect чтобы убедиться, что почему3 знает об alt-er go.

Есть идеи? Может ли кто-нибудь проверить, что этот пример не работает? Любая помощь будет принята с благодарностью!

Ответы [ 2 ]

3 голосов
/ 11 мая 2020

Этот мини-учебник был написан довольно давно, go и не совсем актуален. Новая версия сайта должна появиться в ближайшие месяцы. По сути, этот контракт, а также инвариант для l oop, указанный @iguerNL, должны были проверяться с использованием плагина Jess ie, а не плагина WP Frama- C. Среди различий между этими двумя плагинами, Jess ie не нуждался в предложениях assigns для циклов и функций, в то время как WP они нужны.

Таким образом, полная аннотированная функция max_seq могла бы быть такой: 

/*@ requires n > 0; 
    requires \valid(p+ (0..n−1));
    assigns \nothing;
    ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i]; 
    ensures \exists int e; 0 <= e <= n−1 && \result == p[e]; 
*/ 
int max_seq(int* p, int n) { 
  int res = *p; 
  //@ ghost int e = 0; 
  /*@ loop invariant \forall integer j; 0 <= j < i ==> res >= \at(p[j],Pre); 
      loop invariant \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res; 
      loop invariant 0<=i<=n; 
      loop invariant p==\at(p,Pre)+i; 
      loop invariant 0<=e<n; 
      loop assigns i, res, p, e;
      loop variant n-i;
  */ 
  for(int i = 0; i < n; i++) { 
    if (res < *p) { 
      res = *p; 
      //@ ghost e = i; 
    }
    p++; 
  } 
  return res; 
}

где мы указываем, что функции ничего не назначают в памяти и что l oop назначает различные локальные переменные i, res, p и e (таким образом оставив n без изменений).

Обратите внимание, что доступны более свежие учебные материалы, чтобы узнать об использовании Frama- C с плагином WP. В будущей версии веб-сайта Frama- C упоминается:

0 голосов
/ 07 мая 2020

Вероятно, вы забыли добавить инварианты для «for» l oop. См. Раздел «10.2 L oop Инварианты» в предоставленном вами руководстве (https://frama-c.com/acsl_tutorial_index.html)

...