Как доказать простые равенства недетерминированных значений в Frama-C + EVA?

Меня немного смущает поведение Frama-C версии 18.0 (Argon).

Учитывая следующую программу:

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
    assigns \result \from min, max;
    ensures result_bounded: min <= \result <= max ;
 */
extern int Frama_C_interval(int min, int max);


int main() {

  int i,j;

  i = Frama_C_interval(INT_MIN, INT_MAX);

  j = i;

  assert(j == i);

  return 0;
}

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

frama-c -eva -eva-равенство-домен -eva-полька-равенства foo.c

дает:

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_interval
[eva] using specification for function __FC_assert
[eva:alarm] foo.c:20: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status unknown.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  i ∈ [--..--]
  j ∈ [--..--]
  __retres ∈ {0}

Я что-то пропустил?

Источник

2 ответа

Решение

Интересно. Ваш пример не обработан -eva -eva-equality-domain, который был написан с другими целями. Таким образом, особый случай для x == y когда x а также y Как известно, равных не было написано. Это было бы довольно легко добавить.

(Учитывая имя домена, это может показаться удивительным. Домен равенства больше ориентирован на более широкое распространение в обратном направлении, когда у нас есть неинтересные псевдонимы, например, временные ссылки, добавленные ядром.)

Что касается доменов, поступающих из Apron, это более удивительно. Я изменил ваш пример как таковой:

  j = i;

  int b = j - i;
  int c = j == i;
  Frama_C_dump_each_domain();

Бег frama-c -eva -eva-polka-equalities foo.c -value-msg-key d-apron дает следующий результат:

[eva] c/eq.c:23: 
  Frama_C_dump_each_domain:
  # Cvalue domain:
  i ∈ [--..--]
  j ∈ [--..--]
  b ∈ {0}
  c ∈ {0; 1}
  __retres ∈ UNINITIALIZED
  # Polka linear equalities domain:
  [|-i_44+j_45=0; b_46=0|]

Как вы можете видеть, Фартук предположил связь между i а также j (суффикс - номер строки), упрощенный b до 0, но не упростил c 1. Это удивительно для меня, но объясняет неточность, которую вы наблюдали. Он также не работает с доменом восьмиугольников.

Я не очень знаком с абстрактными преобразователями в реляционных областях, так что этого можно ожидать, но это, безусловно, озадачивает. Код для обработки реляционных операторов существует во Frama-C/Eva/Apron, но частично написан на дому (это не просто вызов примитива Apron). В частности, он вызывает оператор для вычитания и анализирует равенство результата с 0. Трудно понять, почему b было бы точно, но не c,

Источник

Обновление: в более поздних версиях Frama-C (я пробовал с Frama-C 25.0, но он, безусловно, будет работать и в некоторых более старых версиях), домен восьмиугольника может обрабатывать этот конкретный случай:-eva -eva-domains octagonдостаточно, в вашем конкретном коде, чтобы избежать тревоги.

Также обратите внимание, что восьмиугольный домен можно косвенно включить с помощью опции-eva-precision 5(или выше).

Источник
Другие вопросы по тегам