2016-03-22 3 views
0

Я разрабатываю Frama-C-Plugin, это должно печатать значения переменных после каждого утверждения. В Frama-C-Gui, в закладке Values, я могу видеть значения анализа по всей программе и после различных вызовов функций (с параметрами функции).Разработка плагинов Frama-C: получение значений анализа значений разных вызовов

enter image description here

Теперь я хочу, чтобы получить значения после каждого вызова функции (а не «все» -линии, но «главный» -линии.

Вот моя программа, которую я использовал для скриншот:

void swap (int *a, int *b){ 
    int tmp = *a; 
    *a = *b; 
    *b = tmp; 
    return; 
} 
int main (void){ 
    int a=1; 
    int b=2; 
    swap (&a, &b); 

    a = 3; 
    b = 4; 
    swap (&a, &b); 
} 

возможно ли это Как я могу получить доступ к этим значения

PS:? Я задал соответствующий вопрос, который alread y распечатывает «all» -part (и значения ПЕРЕД ПОСТАВКОЙ), см. эту ссылку: Frama-C Plugin development: Getting result of value-analysis

Есть ли подобное решение?

+1

Я считаю, что я, возможно, ответил на это в вашем другом вопросе. Если это так, возможно, стоит закрыть этот (хотя я бы рекомендовал добавить скриншот к другому вопросу с комментарием, например «... как и GUI, как в этой панели», поскольку часто бывает приятно иметь некоторые рисунки в качестве примеров). – anol

+0

Кстати, в идеале, посмотрев исходный код ('src/plugins/value/gui_eval.ml', в этом случае), должно быть возможно вывести хотя бы часть кода (например,' Db.Value. get_stmt_state_callstack' в этом примере, который используется в строках 231 и 235), но я согласен с тем, что для этого часто слишком громоздко. Тем не менее, стоит иметь в виду это, так как он может дать несколько советов о том, какие функции искать в API. – anol

ответ

 Смежные вопросы

  • Нет связанных вопросов^_^