ACSL规范中的命名常量

Question

如何在ACSL规范中使用命名常量？这些常量要么是宏(#define MY_CONST ...)，要么是常量声明(const int MY_CONST ...)。前者不起作用，因为宏没有被预处理器扩展(ACSL规范是C注释)，后者不起作用，因为常量被视为变量，因此某些证明失败。如果我用实际的数字替换命名的常量，那么这个规范就能正常工作。

有没有人有处理命名常量的好主意？提前感谢

Answer 1

为了扩展ACSL规范中的宏，可以使用-pp-annot选项。

Answer 2

我可以在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