Frama-C: Получение выходных данных при использовании указателей

Question

Мне нужно получить список всех выходов функции. Когда я использую From -plugin на следующий код

void add(int *sum, int a, int b) 
{ 
    *sum = a + b; 
} 

int main() 
{ 
    int result; 
    add(&result, 1, 2); 
} 

он говорит мне, что result является выход функции add. Это, конечно, правильно, но я хотел бы, чтобы плагин упоминал sum где-то. Я знаю, что sum является указателем и не изменяется в функции, поэтому он не является выходным, но *sumизменен, и я хотел бы знать это. Есть ли простой (или любой) способ достичь этого?

Answer 1

Если вы установите add в качестве основной точки входа, вы можете быть в состоянии получить информацию, которую вы хотите:

$ frama-c -main add -deps file.c 
[...] 
[from] ====== DEPENDENCIES COMPUTED ====== 
    These dependencies hold at termination for the executions that terminate: 
[from] Function add: 
    S_sum[0] FROM sum; a; b 

В основном, S_sum[0] является *sum: Value (на котором From полагается) генерирует начальное состояние в какие указатели либо NULL, либо указывают на блок с именем, похожим на один из указателей и имеющий по умолчанию два элемента. Существуют параметры командной строки для настройки поведения по умолчанию (см. Value Analysis manual для получения дополнительной информации), но вы можете узнать, что для более сложных примеров вам нужно написать (или сгенерировать) функцию-оболочку, которая будет устанавливать более сложное начальное состояние перед вызовом функции. В этом случае вам нужно будет отслеживать, какой указатель указывает на то, где для восстановления информации.

Основная часть вопроса в том, что в абстрактном состоянии Value, sum отображается на множество L возможных местоположений (здесь сводятся к одноточечному), но *sum не является объект сам по себе. Доступ к записи будет просто обновлять все значения, сопоставленные элементам L. Таким образом, с точки зрения From все выглядит как модификация result (или S_sum[0], если вы меняете точку входа).