Frama-C:在命令行输出中显示调用堆栈

使用值分析插件时，可以使用 GUI 显示给定程序位置的变量值(使用“值”选项卡)。此选项卡中显示的值包括与特定值对应的调用堆栈。例如。:

fn1 -> fn2 -> fn3 | {values}
fn4 -> fn5 -> fn3 | {values}

在命令行上，当分析到达程序位置时，可以使用 Frama_C_show_each(var) 显示变量的值。但是，不会显示相应的调用堆栈。

有没有办法告诉 Frama-C 在给定的程序位置输出调用堆栈以获得 GUI 中的形式(调用堆栈、值)的信息？

非常感谢您的指点。

最佳答案

Eva(前值分析)插件有一个打印调用堆栈的选项:

-val-print-callstacks  When printing a message, also show the current call
                       stack (opposite option is -no-val-print-callstacks)

这以及其他 Eva 选项可通过 frama-c -value-help 或 frama-c -value-h 访问。

否则， this question 包含一个示例脚本，结合 Db.Value.get_stmt_state_callstack ，应该允许制作自定义方式来打印所需的信息。

关于Frama-C:在命令行输出中显示调用堆栈，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/52559038/