Обрабатываются ли бесконечные циклы в Frama-C?

Question

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

void Commit() {
    int count = 1;
    //@ ghost int old_count = 0;

    while (1) {
        //@ ghost old_count = count;
        count++;
        //@ assert count > old_count;
    }
}

int main () {
    Commit();
    return 0;
}

Затем я использую команду: frama-c -val file.c, но статус подтверждения остается неизвестным.Я что-то здесь упускаю?Или бесконечные циклы не обрабатываются Frama-C?

Answer 1

Существует два уровня ответа на ваш вопрос.

1) вы хотите доказать реляционное свойство между old_count и count.Этот вид анализа не доступен по умолчанию в Frama-C / Eva, и ваше утверждение не подтверждается.Вы можете:

• использовать дедуктивную проверку, так как в этом простом примере вам даже не нужны дополнительные аннотации.Вы можете проверить, что frama-c -wp доказывает утверждение

• , используя (экспериментальные) реляционные домены Frama-C / Eva, основанные на Apron.По техническим причинам они еще не работают с утверждениями, поэтому вы должны переписать свой код следующим образом:

  void Commit() {
      int count = 1;
      //@ ghost int old_count = 0;
  
      while (1) {
          //@ ghost old_count = count;
          count++;
          /*@ ghost
            int d = count - old_count;
            Frama_C_show_each(d);
          */
      }
  }
  

  Результат frama-c -val -eva-apron-oct равен

  [value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
  [value] /home/yakobowski/incr.c:5: starting to merge loop iterations
  [value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
  [value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
  [value:alarm] /home/yakobowski/incr.c:7: Warning: 
    signed overflow. assert count + 1 ≤ 2147483647;
  [value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
  

  d всегда имеет значение 1, которое является ожидаемым значением.Без опции -eva-apron-oct вы получите

  [value] /home/yakobowski/incr.c:10: Frama_C_show_each: [-2147483645..2147483646]
  

  на последней итерации.

2) ваш пример не имеет смысла с точки зрения проверки, потому что естьнет таких вещей, как постоянно увеличивающиеся переменные в C. Ваш код верен только до тех пор, пока count < 2147483647.Если вместо этого они равны, ваш код вызывает неопределенное поведение в строке count++.Это и есть причина тревоги, которую Ева издает в этой строке.

Обратите внимание, что этот факт не делает недействительным анализ, который я провел в 1).Все рассуждения, сделанные WP или Eva, основаны на предположении, что count + 1 ≤ 2147483647 верно, что не доказуемо в вашем коде.