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

Posted 2023-03-31

【中文标题】使用 frama-c 的值分析计算函数的可达性

【英文标题】：Calculate reachability to a function using frama-c's value analysis

【发布时间】：2016-05-12 13:44:21

【问题描述】：

这是我的例子：

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]。

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

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

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

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

我使用了全局变量而不是 n。这确实导致了正确的范围，但这个解决方案不能很好地扩展到更复杂的函数和更深的调用堆栈。

【参考方案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 值，性能不会很好。）

【讨论】：

我似乎没有得到正确的结果，log_input 是 [5, MaxInt] 和 log_global [MinInt, MaxInt]，也许这是版本问题？我用的是钠。另外，如果我理解正确，这不适用于未知或非常大的间隔，对吗？

我的错误，Frama_C_interval_split 不是已发布版本的一部分。您可以通过在调用Frama_C_interval 之后编写（繁琐的）ACSL 析取来获得相同的结果：//@ assert n == -10 | n == -9 || ... n == 10。确实，这不适用于大间隔。另一方面，如果您的目标不是全自动，您可以进行智能分区：//@ assert n <= 0 || n > 0 在这种情况下可以工作。