frama-c 停止传播："Assertion got status invalid"

Question

我想为所有断言分割文件 test.c。

test.c 看起来如下：

#include <stdlib.h>

typedef struct {
   float r;
   float g;
   float b;
} Color;

typedef struct {
   int k;
   Color* colors;
} Colors;

void foo(int* a, int k, Colors *colors)
{
    int b=0;   
    colors->colors = (Color*) malloc(k*sizeof(Color));
    //@ assert (colors == NULL);
    if (colors==NULL)
        return;

    colors->k = k;
    int c=10;
    *a=8;
    //@ assert(*a>b);
}

I 运行 frama-c 使用以下命令：

frama-c -slice-assert @all -main foo test.c -then-on 'Slicing export' -print -ocode slice.c

结果 slice.c 如下所示：

/* Generated by Frama-C */
typedef unsigned int size_t;
struct __anonstruct_Color_1 {
   float r ;
   float g ;
   float b ;
};
typedef struct __anonstruct_Color_1 Color;
struct __anonstruct_Colors_2 {
   int k ;
   Color *colors ;
};
typedef struct __anonstruct_Colors_2 Colors;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;

  }
 */
void foo(int *a, Colors *colors)
{
  int b;
  /*@ assert colors ≡ (Colors *)((void *)0); */ ;
  return;
}

查看切片函数 foo，似乎处理不完整。 frama-c 输出告诉我：

test.c:19:[kernel] warning: out of bounds write. assert \valid(&colors->colors);
test.c:20:[value] Assertion got status invalid (stopping propagation).

"status invalid" 是什么意思？当我将第一个断言更改为 //@ assert (colors != NULL);?

时，为什么它会在此处停止传播并起作用

Answer 1

Slicing 插件依赖于 Value Analysis 计算的信息。在其运行期间，Value Analysis 尝试评估其探索的分支上存在的任何 ACSL 注释。您的示例中 assert colors == NULL; 的情况尤其如此，它确实被认为是无效的。

这是为什么？首先，我们可以注意到 colors 是主入口点的形式参数。默认情况下，值分析将创建一个初始状态，其中此类指针是 NULL 或指向两个元素块的指针（有关分析的默认初始状态以及如何使用的更多信息，请参阅 Value's user manual如果需要可以定制）。因此，该断言似乎只会消除第二种可能性，并使 NULL 成为 colors.

的唯一可能性。

然而，函数在到达 assert 之前用 colors 做的另一件事：它在 colors->colors 中赋值。要使此分配有效，colors 需要指向有效的内存位置。因此，您在第 19 行看到的警告（由于历史原因看似由内核发出，但实际上是由 Value 发出），由另一个断言 \valid(&colors->colors) 的生成具体化，您可以看到是否启动 frama-c-gui 与您的选择。

发出警报后，Value 会尝试根据警报减少其内部状态，因为具体执行只有在验证给定条件时才能走得更远（无需冒险进入未定义行为领域）。在我们的例子中，这意味着为 colors 的一组可能值删除 NULL。因此，当我们遇到断言时，我们只有 colors 的一种可能性，并且由于它与断言不匹配，因此状态无效并且传播停止：没有具体的执行可以到达这一点并验证断言。

UPDATE 如果将第一个断言改为//@ assert (colors != NULL);，值分析会发现它是有效的，因为如上所述，到达断言所在的点由于上一条指令中的 colors->colors，只能使用有效的 colors 指针进行评估。因此 Value 继续进行分析，并在正常终止的程序上进行切片，从而得到预期的结果。

关于您的评论，如果在通过注释的程序的任何具体执行期间，ACSL 注释评估为 true，则 ACSL 注释有效，否则无效（如果注释评估为 false，执行应该停止).在实践中，通常不可能（至少在合理的时间 and/or 内存中）执行所有此类评估，因此状态未知，这意味着插件无法决定。请注意，在任何情况下，给定插件发出的状态都取决于该插件的配置。例如，对于 Value，选择的入口点和初始配置会影响 Value 在其抽象执行期间遇到的注释的有效性状态。更准确地说，每次抽象执行到达注释时，状态计算如下：

如果当前抽象状态表示的所有具体状态的注解都为真，则发出有效状态。
如果所有此类具体状态的注解均为假，则发出无效状态，并且此分支的抽象执行停止（因为没有具体执行会通过注解）。
否则状态未知：Value 无法知道注释评估为 false 的具体状态是否真的会在实践中发生，或者只是到目前为止所做的近似值的假象。但是，它会尝试减少其抽象状态以使其表示尽可能少的无效状态（例如，如果您有 /*@ assert 0<= x <= 10;*/ 并且已知 x 在区间 [3; 17] 中，则值将断言后x的间隔使用[3; 10]。

frama-c 停止传播："Assertion got status invalid"

frama-c stops propagation: "Assertion got status invalid"

c

frama-c

program-slicing