ocaml - Frama-C Plugin-Development：获取不同调用的值分析值

Question

我正在开发一个 Frama-C-Plugin，它应该在每个语句之后打印变量的值。在 Frama-C-Gui 的值选项卡中，我可以看到整个程序的分析值，以及在不同的函数调用之后（使用函数的参数）。

我现在想在每个函数调用之后获取值（不是“all”行，而是“main”行。

这是我用于屏幕截图的程序：

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：我问了一个相关的问题，它已经打印了“全部”部分（以及声明之前的值），请参阅此链接： Frama-C 插件开发：获取价值分析的结果

有没有类似的解决方案？

Answer 1

感谢对上述问题答案的编辑，可以在以下站点找到解决方案： Frama-C Plugin development: Getting result of value-analysis