frama-c - FramaC值(value)分析中的slevel选项

Question

我不太明白 FramaC 中的 slevel 选项。谁能解释一下 slevel 的值如何与用户断言(例如 //@assert ...;)或状态相关，以及哪些因素导致状态上升？

例如，我有一个不包含循环但包含if..else分支、go to语句的程序，并且还有一些用户断言程序的一些要点，例如:

...
a = Frama_C_unsigned_int_interval(0, 100);
//@ assert a == 0 || a == 1 || a == 2 || a == 3 || ... || a == 100;
...
b = Frama_C_unsigned_int_interval(a, 200);
//@ assert b == 0 || b == 1 || b == 2 || b == 3 || ... || b == 200;
...

在分析的输出中(我将 slevel 设置为 ~100000)，可能有这样的内容:Semantic level unrolling superposing up up 100 states，然后对于更多的州，此声明可能会重复多次。任何人都可以解释一下这个语义级别展开是如何计算和我怎样才能获得分析的最佳 slevel。谢谢。

Answer 1

值分析执行程序的抽象执行。它不是使用任意值测试程序，而是使用包含所有可能的具体执行的抽象值来执行程序。例如，抽象状态关联 x间隔为 [0;10] .当到达 if语句，例如 if (x<=5) y = 1; else y=2; ，抽象状态根据条件 split 。例如，then分支将以 [0;5] 的间隔执行和 else间隔为 [6;10] 的分支.反之，在整if的最后，你必须加入两个抽象状态。这意味着我们将为每个变量关联一个最小区间，该区间包含来自两个(或更多，例如 switch)父状态的所有可能值。例如，在 if 之后, 我们有 x在 [0;10]和 y在 [1;2] .此外，请注意 Value 看到的是 C 代码的规范化版本，在其中您始终必须为 if 进行分支。 ( { if (c) { s }} 在 Value 中被视为 if (c) { s } else { } 的来源)。

设置-slevel至 N意味着 Value 不会像上面那样加入状态，而是传播到 N单独的状态。在我们的示例中，这意味着我们现在有两种状态，一种是 x在[0;5]和 y==1和其中一个 x在[6;10]和 y==2 .这允许更高的精度(例如，它排除了诸如 x==0 && y == 2 之类的状态)，但是以计算时间和内存消耗为代价。此外，可能的不同状态的数量会随着程序中选择点的数量呈指数增长。事实上，如果你有第二个，无关的，if ，来自第一个的两个状态将被拆分，之后产生 4 个状态(假设 N>=4 )。 Value 指示它正在使用的不同状态的数量，以便您可以在日志中看到 slevel 的位置。花费了，并可能对其进行调整以满足更好的精度/计算时间比。

最后，if不是唯一将国家分开的建筑。任何分支语句，特别是循环，都会导致状态分离。类似地，表示为析取的 ACSL 注释，如您的问题中所示，将具有相同的效果:如果您有足够的 slevel，则析取的每个元素最终都有一个状态。 .