ACSL 仕様で名前付き定数を使用するにはどうすればよいですか? これらの定数は、マクロ ( #define MY_CONST ...) または定数宣言 ( )のいずれかconst int MY_CONST ...です。前者はマクロがプリプロセッサによって展開されないため (ACSL 仕様は C コメントです)、機能しません。後者は、定数が変数として扱われ、一部の証明が失敗するため機能しません。名前付き定数を実際の数値に置き換えると、仕様は正常に機能します。
名前付き定数を処理する良いアイデアはありますか? 前もって感謝します
Pascal Cuoq の助けを借りて問題を解決できました。実際には、frama-c の問題ではなく、gcc の問題です。-fpreprocessed コンパイラ オプションが必要です。私の完全なコマンドは次のとおりです。
frama-c -cpp-extra-args="-I `frama-c -print-share-path`/libc" -cpp-extra-args="-nostdinc" -cpp-extra-args="-fpreprocessed </path/to/stdc-predef.h>" -wp -wp-rte -pp-annot myfile.c