принять моделирование выражения в FramaC

Question

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

#include "/usr/local/share/frama-c/builtin.h" 
 

 
int main(void) 
 
{ 
 
    int selection = Frama_C_interval(0,10); 
 
    int a; 
 
    assume(selection > 5); 
 
    if (selection > 5) 
 
    { 
 
     a = 2; 
 
    } 
 
    else 
 
    { 
 
     a = 1; 
 
    } 
 
    //@ assert a == 2; 
 
    return 0; 
 
}

Я хочу, что значение selection будет больше, чем 5 после этого assume заявления так, что утверждение будет действительным. Моя первоначальная попытка состояла в том, чтобы написать эту функцию void assume(int a){ while(!a); return;} , но это было неудачно. Пожалуйста, помогите мне, спасибо.

Answer 1

Самый простой способ ограничить selection - использовать assert (что, конечно же, не будет подтверждено значением). Если вы хотите, чтобы различать assert, что в действительности гипотезе вы делаете от assert, который вы хотите проверить, вы можете использовать механизм именования ACSL, такой как

//@ assert assumption: selection > 5; 

и убедитесь, что только assert, которые неизвестны являются те, которые называются assumption.

Использование функции assume не может работать как таковое, так как это уменьшит возможное значение параметра a, чтобы быть ненулевым. Значение не может установить связь между значением a в assume и значением selection в main. Тем не менее, это можно немного помочь. Во-первых, -slevel позволяет распространять несколько абстрактных состояний параллельно. Во-вторых, assert, заданный в дизъюнктивной, заставит Value разделить его состояние (если -slevel достаточно большой, чтобы сделать это). Таким образом, с помощью следующего кода

#include "builtin.h" 

void assume(int a) { while(!a); return; } 

int main(void) 
{ 
    int selection = Frama_C_interval(0,10); 
    int a; 
    /*@ assert selection > 5 || selection <= 5; */ 
    assume(selection > 5); 
    if (selection > 5) 
    { 
     a = 2; 
    } 
    else 
    { 
     a = 1; 
    } 
    //@ assert a == 2; 
    return 0; 
} 

и следующую командную строку:

frama-c -cpp-extra-args="-I$(frama-c -print-share-path)" -val -slevel 2 

После того, как первый assert (который, очевидно, действует), Frama-C будет распространяться отдельно два состояния: один, в котором selection > 5 и один, в котором selection <= 5. В первом случае assume вызывается с аргументом 1, поэтому немедленно возвращается, и ветвь thenif берется так, чтобы выполнялся второй assert. Во втором состоянии assume вызывается с 0 и никогда не возвращается. Таким образом, для всех случаев, когда контроль достигает второго assert, он действителен.

Обратите внимание, что вам действительно нужно добавить первый assert внутри тела main, а также скопировать в ACSL аргумент, который вы передаете assume. В противном случае состояние разделения не произойдет (точнее, вы разделите на a, а не на selection).