Frama行为与价值分析

Question

我想使用Frama来分析一个包含read-like函数的程序:给定一个缓冲区buf及其长度len，该函数将len字节准确地写入buf (除非有错误)。

我使用ACSL来指定它，但是值分析给了我奇怪的结果。

下面是我的规范，外加一个用于测试的main函数：

/*@
  assigns \result \from \nothing;
  assigns *(buf+(0..len-1)) \from \nothing;
  behavior ok:
    requires \valid(buf+(0..len-1));
    ensures  \result == 0;
    ensures  \initialized(buf+(0..len-1));
  behavior error:
    ensures  \result == -1;
 */
int read(char *buf, int len);

int main() {
  char buf[10];
  read(buf, 10);
  return 0;
}

在运行frama-c -val test.c (我使用Frama)时，我获得了以下结果：

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization

[value] computing for function read <- main.
        Called from test.c:16.
[value] using specification for function read
test.c:6:[value] Function read, behavior ok: precondition got status valid.
test.c:10:[value] Function read, behavior error: this postcondition evaluates to false in this
        context. If it is valid, either a precondition was not verified for this
        call, or some assigns/from clauses are incomplete (or incorrect).
[value] Done for function read
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  NON TERMINATING FUNCTION

我确实添加了assigns/from子句，并且没有error行为的先决条件(因此，在默认情况下，它们是经过验证的)。

这里发生什么事情？在这种情况下，我怎样才能使分析起作用？

Answer 1

尽管有这条消息，但实际的问题是read函数的规范中有一个错误:这两种行为同时都是活动的，因为它们不包含assumes子句(隐式地，它们都有assumes \true)。因此，两个ensures子句都是真的，这意味着\result == 0 && \result == 1。

此错误导致一种矛盾状态，其中函数的结果同时为0和1(同时)，因此不能返回结果，因此该函数被认为是不终止的。

这里的几种可能的解决方案之一是添加一个不确定的鬼变量(比如_read_state )来表示函数的内部状态，然后使用这个变量为不同的行为定义不相交的assumes子句：

//@ ghost volatile int _read_state;
/*@
  assigns \result \from \nothing;
  assigns *(buf+(0..len-1)) \from \nothing;
  behavior ok:
    assumes _read_state == 0;
    requires \valid(buf+(0..len-1));
    ensures  \result == 0;
    ensures  \initialized(buf+(0..len-1));
  behavior error:
    assumes _read_state != 0;
    ensures  \result == -1;
 */

注意，== 0和!= 0比较是任意的；任何一组可能不相交的值都可以在这里工作。

使用此规范，我们获得了该程序的预期结果：

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
  _read_state ∈ [--..--]
[value] computing for function read <- main.
        Called from test.c:18.
[value] using specification for function read
tread.c:7:[value] Function read, behavior ok: 
    precondition got status valid. 
    (Behavior may be inactive, no reduction performed.)
[value] Done for function read
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  buf[0..9] ∈ [--..--] or UNINITIALIZED
  __retres ∈ {0}