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

Question

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

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].

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

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

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

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

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

Answer 1

Вот возможное решение. Используйте встроенный 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.)