小编dor*_*dow的帖子

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

有没有人有一个好主意来处理命名常量？提前致谢