Расчет достижимости функции с помощью анализа значений frama-c

Вот мой пример:

int in;
int sum(int n){
    int log_input = n;
    int log_global = in;
    return 0;
}

int main(){
    int n = Frama_C_interval(-10, 10);
    in = n;
    if (n > 0){
        sum(n + 4);
    }
    return 0;
}

Что я хотел бы сделать, так это найти диапазон входной переменной n при инициализации в main, что приводит к достижению суммы функции. Правильный диапазон в этом примере - [1, 10].

В этом примере я хотел бы «сохранить» исходный ввод в глобальном значении in и повторно ввести его в функцию sum, присвоив его переменной log_global и, таким образом, обнаружение исходного ввода, в результате которого была достигнута функция. При запуске frama-c в этом примере мы получаем, что диапазон log_input равен [5, 14], а диапазон log_global равен [-10, 10]. Я понимаю, почему это происходит - значение in устанавливается в начале main и на него не влияют дальнейшие манипуляции с n.

Мне было интересно, есть ли простой способ изменить это во frama-c? Может быть, простая модификация кода frama-c?

У меня была одна не связанная с этим идея - манипулировать оператором if в main:

if (in > 0){
    sum(in + 4);
}

Я использовал глобальную переменную вместо n. Это действительно приводит к правильному диапазону, но это решение плохо масштабируется для более сложных функций и более глубоких стеков вызовов.


c frama-c abstract-interpretation
person Maor Veitsman    schedule 03.02.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вот возможное решение. Используйте встроенный Frama_C_interval_split и соответствующий -slevel N (здесь хотя бы N=21). Функция sum будет проверена N раз, по одному для каждого возможного значения N, и результат будет точным.

int n = Frama_C_interval_split(-10, 10);

Результаты:

 [value] Values at end of function sum:
  log_input ∈ [5..14]
  log_global ∈ [1..10]
  __retres ∈ {0}

(По сути, это означает выполнение ручной проверки модели, поэтому производительность не будет хорошей для больших значений N.)

person byako    schedule 03.02.2016
comment
Кажется, я не получаю правильные результаты, log_input - [5, MaxInt] и log_global [MinInt, MaxInt], возможно, это проблема версии? Я использую натрий. Также, если я правильно понимаю, это не применимо к неизвестным или очень большим интервалам, не так ли? - person Maor Veitsman; 04.02.2016
comment
Моя ошибка, Frama_C_interval_split не входит в выпущенную версию. Вы можете получить тот же результат, написав (утомительную) дизъюнкцию ACSL после вызова Frama_C_interval: //@ assert n == -10 | n == -9 || ... n == 10. И действительно, для больших интервалов это не сработает. С другой стороны, если вы не стремитесь к полной автоматичности, вы можете провести разумное разбиение: //@ assert n <= 0 || n > 0 в этом случае будет работать. - person byako; 04.02.2016