Named constants in ACSL specifications

Question

How can I make use of named constants in ACSL specifications? These constants are either Macros (#define MY_CONST ...) or constant declarations (const int MY_CONST ...). The former does not work since the macros are not expanded by the preprocessor (ACSL specs are C comments), the latter does not because the constants are treated as variables so that some proofs fail. The specification works fine if I replace the named constants with the actual numbers.

Does anyone have a good idea to handle named constants? Thanks in advance

Answer 1

In order to expand macros in ACSL specification, you can use the -pp-annot option.