使用 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 中初始化时导致达到函数 sum 的输入变量 n 的范围。此示例中的正确范围是 [1, 10]。

在示例中，我想将原始输入“保存”在全局值 in 中，然后通过将其分配给变量 log_global 将其重新引入函数 sum > 从而发现导致到达函数的原始输入。在此示例上运行 frama-c 时，我们得到 log_input 的范围是 [5, 14]，log_global 的范围是 [-10, 10]。我明白为什么会发生这种情况 - in 的值设置在 ma​​in 的开头，并且不受 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 的可能值一次，结果将是精确的

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 值，性能不会很好。)