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

Question

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

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

示例:

volatile int x = 0;

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

这里 frama-c 检测到 x 是 volatile 的，因此具有范围 [--..--]，但我知道另一个线程将写入 x 的内容，并且我想告诉分析器 x 只能为 0或 1。 这对于 frama-c 来说可能吗，尤其是在 GUI 中？

提前致谢 克里斯蒂安

Answer 1

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

int x = 0;

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

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