使用frama-c的值分析计算函数的可达性

Question

这是我的例子:

int in;
int sum(int n){
    int log_input = n;
    int log_global = in;
    return 0;
}

int main(){
    int n = Frama_C_interval(-10, 10);
    in = n;
    if (n > 0){
        sum(n + 4);
    }
    return 0;
}

我想要做的是在main中初始化时找到输入变量n的范围,从而得到函数sum.此示例中的正确范围是[1,10].

在示例中,我想将原始输入"保存"在全局值中,并通过将其分配到变量log_global中来重新引入它,从而发现导致到达函数的原始输入.在此示例上运行frama-c时,我们得到log_input的范围是[5,14],log_global的范围是[-10,10].我理解为什么会发生这种情况 - in的值设置在main的开头,并且不受对n的进一步操作的影响.

我想知道在frama-c中是否有一种简单的方法可以改变它？也许是对frama-c代码的一个简单修改？

我有一个不相关的想法是操纵main中的if语句:

if (in > 0){
    sum(in + 4);
}

我使用全局变量而不是n.这确实产生了正确的范围,但是这种解决方案不能很好地扩展到更复杂的功能和更深的调用堆栈.

Answer 1

这是一个可能的解决方案。使用内置函数Frama_C_interval_split和适当的函数-slevel N（至少在这里N=21）。该函数sum将被检查 N 次，针对 N 的每个可能值检查一次，结果将是精确的

\n\n

int n = Frama_C_interval_split(-10, 10);\n

\n\n

结果：

\n\n

 [value] Values at end of function sum:\n  log_input \xe2\x88\x88 [5..14]\n  log_global \xe2\x88\x88 [1..10]\n  __retres \xe2\x88\x88 {0}\n

\n\n

（基本上，这相当于执行手动模型检查，因此对于较大的 N 值，性能不会很好。）

\n