Понимание результатов среза 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 возвращает следующий фрагмент (который является точным), используя критерий "f -slice-return" и f в качестве точки входа:

/*@ 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;
}

)

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

С Уважением,

Ромен

Редактировать: я написал "еще, если (a!= 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 не позволяет ссылаться на значение формальных переменных в пост-состоянии, главным образом потому, что это бессмысленно с точки зрения вызывающей стороны. (Кадр стека вызываемого абонента извлекается после завершения вызова.)