FramaC价值分析中的一些选择

Question

我不太了解slevelFramaC中的选项.任何人都可以解释更多关于如何与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 to 100 states,然后这个语句可能会重复多次,状态更多.有谁可以解释这是如何semantic level unrolling计算的,我如何获得最佳slevel的分析.谢谢.

Answer 1

值分析执行程序的抽象执行.它不是使用任意值测试程序,而是使用包含所有可能的具体执行的抽象值来执行它.例如,抽象状态x与间隔相关联[0;10].if例如if (x<=5) y = 1; else y=2;,当到达一个语句时,根据条件分割抽象状态.例如,所述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.