frama-c停止传播：“断言获取状态无效”

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);
}

我使用以下命令运行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).

“状态无效”是什么意思？当我将第一个断言更改为//@ assert (colors != NULL);时，它为什么停止在这里传播？

Answer 1

切片插件依赖于通过值分析计算的信息。在运行过程中，Value试图评估它所探索的分支上的任何ACSL注释。在您的示例中，assert colors == NULL;的情况尤其如此，它确实被认为是无效的。

为什么会这样呢？首先，我们可以注意到，colors是主入口点的正式论证。默认情况下，值分析将创建一个初始状态，其中这种指针要么是NULL，要么是指向两个元素块的指针(有关分析的默认初始状态的更多信息，以及如何在需要的情况下对其进行定制)，请参见价值用户手册。因此，断言似乎只是删除了第二种可能性，并将NULL保留为colors的唯一可能性。

然而，在到达colors之前，该函数还需要对assert做另一件事情:它在colors->colors中分配一些东西。要使此赋值有效，colors需要指向一个有效的内存位置。因此，您在第19行中看到的警告(似乎是内核出于历史原因发出的，但实际上是由值发出的)通过生成另一个断言\valid(&colors->colors)实现的，您可以看到是否使用选项启动frama-c-gui。

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

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

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

• 如果注释对于当前抽象状态表示的所有具体状态都是真的，则发出有效状态。
• 如果注释对于所有这些具体状态都是假的，则发出无效状态，并且该分支的抽象执行将停止(因为没有任何具体的执行会通过注释)。
• 否则，状态是未知的: Value无法知道注释计算为false的具体状态在实践中是否真的会发生，还是仅仅是迄今为止所做的近似的一种假象。但是，它试图减少其抽象状态，使其尽可能少地表示无效状态(例如，如果您有/*@ assert 0<= x <= 10;*/，而x位于[3; 17]区间，则在断言之后，值将使用[3; 10]作为x的间隔)。