Дьявол кроется в деталях, но это может сработать для вас:
Сначала получите Frama-C . Если вы используете Unix, ваш дистрибутив может иметь пакет. Пакет не будет последней версией, но может быть достаточно хорошим и сэкономит вам время, если вы установите его таким образом.
Скажем, ваш пример такой, как приведенный ниже, только настолько большой, что не очевидно, что не так:
int add(int x, int y)
{
static int state;
int result = x + y + state; // I tested it once and it worked.
state++;
return result;
}
Введите команду, например:
frama-c -lib-entry -main add -deps ugly.c
Опции -lib-entry -main add
означают «посмотрите на функцию add
». Опция -deps
вычисляет функциональные зависимости. Вы найдете эти «функциональные зависимости» в журнале:
[from] Function add:
state FROM state; (and default:false)
\result FROM x; y; state; (and default:false)
Здесь перечислены фактические входные данные, от которых зависят результаты add
, и фактические выходные данные, вычисленные из этих входных данных, включая статические переменные, считанные и измененные. Статическая переменная, которая была должным образом инициализирована перед использованием, обычно не будет отображаться в качестве входных данных, если только анализатор не сможет определить, что она всегда была инициализирована перед чтением из.
Журнал показывает state
как зависимость \result
. Если вы ожидали, что возвращаемый результат будет зависеть только от аргументов (то есть два вызова с одинаковыми аргументами приводят к одному и тому же результату), это подсказка, что здесь может быть что-то не так с переменной state
.
Еще одна подсказка, показанная в приведенных выше строках, заключается в том, что функция изменяет state
.
Это может помочь или нет. Опция -lib-entry
означает, что анализатор не предполагает, что какая-либо неконстантная статическая переменная сохранила свое значение во время вызова анализируемой функции, что может быть слишком неточным для вашего кода. Есть способы обойти это, но тогда вам решать, хотите ли вы играть в азартные игры время, необходимое для изучения этих способов.
РЕДАКТИРОВАТЬ: вот более сложный пример:
void initialize_1(int *p)
{
*p = 0;
}
void initialize_2(int *p)
{
*p; // I made a mistake here.
}
int add(int x, int y)
{
static int state1;
static int state2;
initialize_1(&state1);
initialize_2(&state2);
// This is safe because I have initialized state1 and state2:
int result = x + y + state1 + state2;
state1++;
state2++;
return result;
}
В этом примере та же команда выдает результаты:
[from] Function initialize_1:
state1 FROM p
[from] Function initialize_2:
[from] Function add:
state1 FROM \nothing
state2 FROM state2
\result FROM x; y; state2
То, что вы видите для initialize_2
- это пустой список зависимостей, означающий, что функция ничего не назначает. Я поясню этот случай, отображая явное сообщение, а не просто пустой список. Если вы знаете, что должна делать любая из функций initialize_1
, initialize_2
или add
, вы можете сравнить это априорное знание с результатами анализа и увидеть, что что-то не так для initialize_2
и add
.
ВТОРОЕ РЕДАКТИРОВАНИЕ: и теперь мой пример показывает что-то странное для initialize_1
, поэтому, возможно, я должен объяснить это. Переменная state1
зависит от p
в том смысле, что p
используется для записи в state1
, а если бы p
было другим, то окончательное значение state1
было бы другим. Вот последний пример:
int t[10];
void initialize_index(int i)
{
t[i] = 1;
}
int main(int argc, char **argv)
{
initialize_index(argv[1][0]-'0');
}
С помощью команды frama-c -deps t.c
зависимости, вычисленные для initialize_index
:
[from] Function initialize_index:
t[0..9] FROM i (and SELF)
Это означает, что каждая из ячеек зависит от i
(его можно изменить, если i
является индексом этой конкретной ячейки). Каждая ячейка также может сохранять свое значение (если i
обозначает другую ячейку): это указывается с пометкой (and SELF)
в последней версии и помечается более неясным (and default:true)
в предыдущих версиях.