Тестирование промежуточных переменных в большом файле с использованием Frama-c

Question

Я пытаюсь использовать Frama-c, чтобы проверить некоторые свойства функции C, которая у меня есть.Функция довольно большая, и есть несколько промежуточных переменных, которые мне нужно проверить.(Я слежу за этим и этим руководством)

Моя программа имеет следующую структуру:

1. По всему объему 15 операторов returnпрограмма.

2. Переменным, которые мне нужно проверить, являются назначенные значения в нескольких местах программы, в зависимости от пути программы.

   my_function(){
   intermediate var 1=xx;
   //@assert var 1>some_value;
   intermediate var 2=yy;
   
   return var 4;
   
   intermediate var 1=xx;
   //@assert var 1>some_value;
   return var 4;
   
   intermediate var 2=xx;            
   intermediate var 1=yy;
   //@assert var 1>some_value;
   
   return var 4;
   }
   

Объяснение : Мне нужно проверить определенные свойства, связанные с вар 1, вар 2 и вар 4. Я пробовал 2 подхода.

1. использовать assert всякий раз, когда вар 1 установлен, как указано выше.

Проблема в том, что Frama-C проверяет только первое утверждение.

использовать аннотации в начале.

/*@ requires \valid(var 1);
   ensures var 1 > some_value;
 */

В этом случае Frama-C возвращает ошибку.

Вопрос : Как проверить свойства для промежуточных задач?Есть ли пример программы?

* Я не включил свою исходную функцию, так как она очень длинная.

Answer 1

Как уже упоминал Вирджил, ваш вопрос не очень ясен, но я предполагаю, что вы пытаетесь проверить некоторые свойства var1 и var2.Эта книга содержит несколько хороших примеров, и я думаю, что вам поможет следующее:

int abs(int val){
    int res;
    if(val < 0){
    //@ assert val < 0 ;
    res = - val;
    //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val;
    } else {
    //@ assert !(val < 0) ;
    res = val;
    //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val;

    }    
    return res;
}

Автор использовал концепцию троек Хоара в этом сценарии, где вы проверяете (утверждаете)определенное свойство, утверждая его требования (предварительное условие) для свойства и проверяя, сохраняется ли свойство после выполнения соответствующих операторов.

Надеюсь, это поможет.