c - Frama-C と WP-Plugin を使用した Reads 句

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 ではまだ実装されていません。他にどのような代替手段がありますか?

string.h からいくつかの関数を証明するために、この公理が必要です (例: strcmp)

Answer 1

Frama-C/Wp の Oxygen バージョンでは、(ACSL の観点からは正しくありませんが)そのような状況でreads *s代わりに使用しても安全です。reads s[..]

Frama-C の次のリリースでは、一般的な読み取り句が有効になります。