Понимание результатов резки Frama-C

Question

Хотелось бы узнать, можно ли сделать какой-либо предварительный обработанный срез с помощью Frama-C, и я играю с некоторыми примерами, чтобы понять, как это можно достичь.

У меня есть этот простой пример, который, кажется, приводит к неточному срезу, и я не могу понять, почему. Вот функция, я хотел бы порезать:

int f(int a){ 
int x; 
if(a == 0) 
    x = 0; 
else if(a != 0) 
    x = 1; 
return x; 
} 

Если я использую эту спецификацию:

/*@ requires a == 0; 
    @ ensures \old(a) == a; 
    @ ensures \result == 0; 
*/ 

затем Frama-C возвращает следующий фрагмент (который является точным), используя «е -slice -Возвращение»критерий и е в качестве точки входа:

/*@ ensures \result ≡ 0; */ 
int f(void){ 
    int x; 
    x = 0; 
    return x; 
} 

Но при использовании этой спецификации:

/*@ requires a != 0; 
    @ ensures \old(a) == a; 
    @ ensures \result == 1; 
*/ 

тогда все инструкции (& аннотаций) остаются (когда я ждал этого кусочка быть возвращено:

/*@ ensures \result ≡ 1; */ 
int f(void){ 
    int x; 
    x = 1; 
return x; 
} 

)

В последнем случае, это срез неточный? В этом случае, что может быть причиной?

С уважением,

Romain

Edit: я написал "еще, если (а = 0!) ...", но проблема остается "еще ..."

Answer 1

В Frama- C, плагин для зависания зависит от результата предварительного статического анализа, называемого анализом значений. Анализ

---

Это значение может представлять значения для переменной a при a == 0 (множество значений в этом случае { 0 }), но имеет трудное время для представления значения для a, когда известно, что a != 0. В последнем случае, если a еще не известен как положительный или отрицательный, плагин анализа стоимости должен аппроксимировать набор значений для a. Если известно, что a является положительным, например, если оно было unsigned int, то ненулевые значения могут быть представлены как интервал, но плагин анализа стоимости не может представлять «все значения типа int, кроме 0».

---

Если вы готовы изменить предварительное условие, вы можете записать его в форме, более понятный анализ стоимости плагина (вместе со значением опцией анализа -slevel):

$ cat t.c 
/*@ requires a < 0 || a > 0 ; 
    @ ensures \old(a) == a; 
    @ ensures \result == 0; 
*/ 

int f(int a){ 
int x; 
if(a == 0) 
    x = 0; 
else if(a != 0) 
    x = 1; 
return x; 
} 
$ frama-c -slevel 10 t.c -main f -slice-return f -then-on 'Slicing export' -print 
… 
/* Generated by Frama-C */ 
/*@ ensures \result ≡ 0; */ 
int f(void) 
{ 
    int x; 
    x = 1; 
    return x; 
} 

Answer 2

Это не имеет никакого отношения к вашему основному вопросу, но ваш пункт ensures a == \old(a) не делает то, что вы ожидаете. Если вы печатаете свой исходный код с опцией -print, вы увидите, что он был безшовно преобразован в ensures \old(a) == \old(a).

Язык ACSL не позволяет ссылаться на значение формальных переменных в пост-состоянии, главным образом потому, что это не имеет смысла с точки зрения вызывающего. (Рамка стека вызываемого абонента выскочит после завершения вызова.)