c - 使用 Frama-C 和 WP-Plugin 读取子句

Question

在为字符串长度定义公理时，我需要使用reads 子句。

/*@
predicate Length_of_str_is{L}(char *s, integer n) =
 (0 <= n) && \valid(s+(0..n)) && s[n] == 0 &&
 \forall integer i; 0 <= i < n ==> s[i] != 0;

axiomatic LengthAxiomatic{
    logic integer Length{L}(char *s) reads s[..];
    axiom str_length{L}:
    \forall integer n, char *s; Length_of_str_is(s, n) ==> Length(s) == n;
}
@*/

但是，WP中还没有实现任意区域的reads子句，还有什么其他的选择呢？

我需要这个公理来证明 string.h 中的一些函数(例如:strcmp)

Answer 1

在 Frama-C/Wp 的 Oxygen 版本下，它是安全的(尽管从 ACSL 的角度来看不正确)
使用 reads *s而不是 reads s[..]在这种情况下。

下一个即将发布的 Frama-C 版本将启用通用读取子句。