Сделайте зависимости от изображения Frama-c даже от «мертвых ветвей»

Question

Я использую версию frama-c Aluminium-20160502, и я хочу узнать зависимости в большой программе. При использовании опции -deps в командной строке я обнаружил, что некоторые зависимости отсутствуют. В частности, когда несколько условий объединяются в один, если анализ зависимости останавливается всякий раз, когда одно условие ложно. В этом примере здесь:

#include<stdio.h> 
#include<stdbool.h> 

/*Global variable definitions*/ 
bool A = true; 
bool B = false; 
bool C = true; 
bool X; 
bool Y; 

bool res; 


void main(){ 

     if (A && B && C) { 
       res = X; 
     }else res = Y; 
} 

когда я пытаюсь: frama-c -deps program.c

Frama показывает следующие зависимости:

[от] ====== ЗАВИСИМОСТИ COMPUTED ======

Эти зависимости сохраняются при завершении для выполнения, которые завершаются:

[from] Функция main: res FROM A; B; Y

[от] ====== END зависимостей ======

поэтому не достигает условие С, потому что уже B ложно.

Интересно, есть ли способ сообщить Frama для вычисления всех зависимостей, даже если условие не выполняется. Я пробовал с опцией -slevel, но без каких-либо результатов. Я знаю, что есть способ использовать интервал Frama_C_interval (0,1), но когда я его использую, переменная, использующая эту функцию, не отображается в зависимостях. Я хотел бы получить X и Y, зависящие от A, B, C и res, зависящие от A, B, C, X, Y

Любые идеи?

Answer 1

Плагин From использует результаты плагина анализа значений. В вашем примере значения A и B достаточно точны, что Значение позволяет сделать вывод, что условие полностью определено (поскольку оператор && лениво оценивается слева направо) до достижения C, поэтому C никогда не влияет на результат и следовательно, не является зависимостью с точки зрения От.

К сожалению, Frama_C_interval не может быть использован непосредственно на глобальных инициализаторах:

user error: Call to Frama_C_interval in constant. 

Вы можете, однако, использовать "взломать" (не всегда лучшее решение, но здесь работает):

volatile bool nondet; 
bool A = nondet; 
bool B = nondet; 
bool C = nondet; 
... 

Обратите внимание, что поскольку nondet равно volatile, каждой переменной A, B и C присваивается другое недетерминированное значение.

В этом случае стоимость должна учитывать обе ветви условными, и поэтому C становится зависимость в вашем примере, так как возможно, что C будет читаться во время выполнения main. После этого вы будете иметь:

 These dependencies hold at termination for the executions that terminate: 
[from] Function main: 
    res FROM A; B; C; X; Y 

Обратите внимание, что некоторые плагины требуют специальной обработки при работе с летучими переменными, так что это не всегда является лучшим решением.

Это, однако, касается только некоторых видов зависимостей.Как упоминалось в главе 6 раздела Value Analysis user manual, плагин From вычисляет функциональные, императивные и операционные зависимости. Они делают не включают косвенные управляющие зависимости, которые являются такими, как X from A, B, C, как вы упомянули. Для них нужен плагин PDG (Program Dependence Graph), но в настоящее время он не имеет текстового вывода зависимостей. Вы можете использовать -pdg, чтобы вычислить его, а затем -pdg-dot <file>, чтобы экспортировать граф зависимостей в формате dot (graphviz). Вот что я получаю за main функции (с помощью летучего хак, как уже упоминалось ранее):

Наконец, в качестве примечания: -slevel в основном используется для улучшения точности, но в вашем примере вы уже имеют слишком много точность (то есть, значение уже может сделать вывод, что C никогда не читается внутри main).