标签: value-analysis

我需要使用frama-c值分析插件来分析一些项目。这些项目使用 CMake 构建基础设施作为它们的构建系统。

我使用 frama-c 分别分析每个文件。这样，入口点的信息就会丢失。更准确地说，frama-c 需要一个不包含“main”函数的文件的入口点，因此覆盖所有函数并在项目的单个文件中选择最佳入口点是一项挑战。

我的问题是，有没有一种方法可以将整个项目作为一个整体（而不是逐个文件）运行 frama-c ？

在EVA教程中,我找到了这个截图: 解释:"导致这一点的确切值显示在第c5列:-1.C标准将负数的左移视为未定义的行为.因为-1是此callstack中唯一可能的值,所以减少由警报引起的后状态就是这样."

所以,我想问:

Frama-C EVA插件中"后"栏的含义和目的是什么？

有没有更详细的文件来理解EVA中使用的术语"减少"和"后状态"？

我正在使用价值分析为Frama-C制作插件.我只想在每个语句之后打印变量(值)的状态(我认为解决方案很容易安静,但我无法弄明白).

我在访问者Db.Value.get_stmt_state的vstmt_aux方法中获得了当前状态.

我现在如何获得变量的值？

PS:我发现这篇文章,但它没有帮助,没有真正的解决方案,并且在描述的帮助下我无法做到: 如何在Value.Eval_expr,Value.Eval_op等模块中使用函数Frama-c Value插件