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;
}
@*/

但是，任意区域的 reads 子句在 WP 中还没有实现，还有哪些替代方案呢？

我需要这个公理来证明 string.h 中的一些函数（例如：strcmp）

Answer 1

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

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