static-analysis - 是否可以在 frama-c 值分析器中注入值？

Question

我正在尝试使用 frama-c 值分析器来评估实际上是线程化的 C 代码。我想忽略任何可能发生的线程问题，只检查单个线程的可能值。到目前为止，这是通过将入口点设置为线程开始的位置来实现的。

现在我的问题是：在一个线程中，我读取由另一个线程写入的值，因为 frama-c 不（也不应该？）考虑线程（当前）它假设我的变量在某个广泛的范围内，但我知道范围实际上要小得多。是否可以告诉值分析器这个变量的值范围？

例子：

volatile int x = 0;

void f() {
    while(x==0)
        sleep(100);
    ...
}

这里 frama-c 检测到 x 是易失的，因此具有范围 [--..--]，但我知道另一个线程将写入 x 的内容，我想告诉分析器 x 只能是 0 或 1。这对frama-c是否可行，尤其是在gui中？

在此先感谢基督教

score 3 · Accepted Answer

这目前无法自动实现。值分析认为 volatile 变量始终包含其基础类型中包含的全部值。然而，存在一个专有插件，它将对 volatile 变量的访问转换为对用户提供的函数的调用。在您的情况下，您的代码将基本上转换为：

int x = 0;

void f() {
while(1) {
    x = f_volatile_x();
    if (x == 0)
    sleep(100);
...
}

通过f_volatile_x正确指定，您可以确保它只返回 0 到 1 之间的值。

score 2 · Accepted Answer

如果您正在研究的线程中未修改变量“x”，您还可以在“main”函数的开头使用以下命令对其进行初始化：

x = Frama_C_interval (0, 1);

这是一个由 Frama-C 定义的函数，...../share/frama-c/builtin.c因此您必须在使用它时将此文件添加到您的输入中。

2 回答 2