Frama-C行为和价值分析

Question

我想用Frama-C分析一个包含一个类似于 read 的函数：给定缓冲区 buf 及其长度 len，该函数在 buf 中准确写入 len 个字节（除非出现错误） .

我是用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-C Neon）时，我得到了这个结果：

[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.

这个错误导致了一个矛盾的状态，其中 function 既是 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}

Frama-C行为和价值分析

Frama-C behaviors and value analysis

frama-c