问题标签 [value-analysis]

我的实体数据模型包含有关哪些字段可以为空和不可为空的信息。但是，生成的模板不包含此信息。

在我的代码的其他地方，我JetBrains.Annotations用来显示允许空值的位置和不允许空值的位置。例如：

如何使 Entity Framework 生成包含这些值分析属性的代码？

我正在通过DbContext.

当使用一些基准运行 Frama-C 值分析时，例如susan在 中http://www.eecs.umich.edu/mibench/automotive.tar.gz，我们注意到很多块被认为是死代码或无法访问。然而，在实践中，这些代码是在我们从这些块中打印出一些调试信息时执行的。有没有人注意到这个问题？我们如何解决这个问题？

假设我们有以下 C 代码：

我想在初始化时使用静态分析计算变量 x 的边界，从而得到满足的谓词。在这个例子中，main 开头的 x 的间隔应该是 [8, 12]。

TL;DR：给定代码中某处的断言，计算这些范围的最佳方法是什么？

到目前为止我尝试了什么：

我认为解决这个问题的最佳方法是使用最弱的前提条件计算器。我尝试过使用 frama-c 的 wp 插件，但由于它是为验证目的而构建的，我不确定它在这个用例中有多有用。在以下代码上应用插件时：

我收到以下谓词发送到 alt-ergo 求解器：

如果您仔细观察，可以通过遵循变量 i 上不会导致 (i_1 = 0) 的边界来识别输入所需的间隔。我已经标记了这些界限。这不是很健壮，例如，如果断言更改为&& n <= 13，则隐含谓词的“左侧”保持不变，因为没有任何条件改变。另外我不确定这在其他情况下有多大用处，例如在调用函数时将我的断言更改为 requires 语句，我无法理解生成的谓词：

并向函数添加 requires 语句：

我得到：

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

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

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

我正在分析具有以下结构的控制程序：

我的目标是分析足够的循环迭代以表明 cnt 变量不会溢出。单独增加 slevel 无济于事，因为状态空间会变得太高。我看到可以针对各个功能调整 slevel。这对于例如单个 if/else 构造是否也是可能的？对于这样的循环结构，增加整个函数的 slevel 可能已经太多了。有没有办法在不编写复杂的循环不变量和断言的情况下证明不存在溢出？

BR，哈拉尔

我正在使用价值分析为 Frama-C 开发插件。我只是想在每个语句之后打印变量（值）的状态（我认为解决方案很简单，但我想不通）。

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

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

PS：我找到了这个帖子，但没有帮助，没有真正的解决方案，并且在描述的帮助下我无法做到： How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c 价值插件

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

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

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

这可能吗？如何访问这些值？

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

有没有类似的解决方案？

在下面的程序中，函数dec用于scanf读取用户的任意输入。

dec被调用main并根据输入返回 1 或 0，因此将执行操作。但是，值分析表明y始终是0，即使在调用 之后也是如此scanf。这是为什么？

在EVA 教程中，我找到了这个屏幕截图：带有解释：“导致这种情况的确切值显示在 c5 列中：-1。C 标准将负数的左移视为未定义行为。因为 -1 是此调用堆栈中唯一可能的值，由警报引起的减少导致后状态为 ."

所以，我想问：

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

是否有更详细的文件来理解 EVA 中使用的“减少”和“后状态”一词？