Я разрабатываю Frama-C-Plugin, это должно печатать значения переменных после каждого утверждения. В Frama-C-Gui, в закладке Values, я могу видеть значения анализа по всей программе и после различных вызовов функций (с параметрами функции).Разработка плагинов Frama-C: получение значений анализа значений разных вызовов
Теперь я хочу, чтобы получить значения после каждого вызова функции (а не «все» -линии, но «главный» -линии.
Вот моя программа, которую я использовал для скриншот:
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
Есть ли подобное решение?
Я считаю, что я, возможно, ответил на это в вашем другом вопросе. Если это так, возможно, стоит закрыть этот (хотя я бы рекомендовал добавить скриншот к другому вопросу с комментарием, например «... как и GUI, как в этой панели», поскольку часто бывает приятно иметь некоторые рисунки в качестве примеров). – anol
Кстати, в идеале, посмотрев исходный код ('src/plugins/value/gui_eval.ml', в этом случае), должно быть возможно вывести хотя бы часть кода (например,' Db.Value. get_stmt_state_callstack' в этом примере, который используется в строках 231 и 235), но я согласен с тем, что для этого часто слишком громоздко. Тем не менее, стоит иметь в виду это, так как он может дать несколько советов о том, какие функции искать в API. – anol