1

我想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;
}

查看 sliced function 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);？

4

1 回答 1

3

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

这是为什么？首先，我们可以注意到colors主入口点是一个形式参数。默认情况下，Value Analysis 将创建一个初始状态，其中此类指针是NULL或指向两个元素块的指针（有关分析的默认初始状态以及如何在需要时自定义的更多信息，请参阅Value 的用户手册） . 因此，该断言似乎只是删除了第二种可能性并保留NULL为 的唯一可能性colors。

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

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

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

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

  • 如果注释对于当前抽象状态表示的所有具体状态都为真，则发出有效状态。
  • 如果所有这些具体状态的注释为假，则发出无效状态，并且该分支的抽象执行停止（因为没有具体执行会通过注释）。
  • 否则状态未知：Value 无法知道注释评估为 false 的具体状态是否真的会在实践中发生，或者只是迄今为止所做的近似的假象。但是，它试图减少其抽象状态以使其表示尽可能少的无效状态（例如，如果您有/*@ assert 0<= x <= 10;*/并且x已知在区间内[3; 17]，则 Value 将用于断言之后的[3; 10]区间）。x
于 2016-07-18T06:56:59.980 回答