如何在ACSL规范中使用命名常量？这些常量是宏(#define MY_CONST ...)或常量声明(const int MY_CONST ...).前者不起作用,因为预处理器没有扩展宏(ACSL规范是C注释),后者不是因为常量被视为变量,因此一些证明失败.如果我用实际数字替换命名常量,规范工作正常.
有没有人有一个好主意来处理命名常量？提前致谢
| 归档时间： |
|
| 查看次数： |
154 次 |
| 最近记录： |