6

这是我的例子：

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并将其重新引入函数 sum 中，从而发现导致到达函数的原始输入。在这个示例上运行 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。这确实导致了正确的范围，但是这个解决方案不能很好地扩展到更复杂的函数和更深的调用堆栈。

4

1 回答 1

3

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

int n = Frama_C_interval_split(-10, 10);

结果：

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

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

于 2016-02-03T16:37:10.733 回答