如何在 ACSL 规范中使用命名常量？这些常量要么是宏 ( #define MY_CONST ...) 要么是常量声明 ( const int MY_CONST ...)。前者不起作用，因为预处理器没有扩展宏（ACSL 规范是 C 注释），后者不起作用，因为常量被视为变量，因此某些证明失败。如果我用实际数字替换命名常量，规范就可以正常工作。
有没有人有处理命名常量的好主意？提前致谢
问问题
174 次
2 回答
6
为了扩展 ACSL 规范中的宏，您可以使用该-pp-annot选项。
于 2014-03-17T07:28:07.243 回答
1
我可以在 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
于 2014-04-01T19:42:44.020 回答