Using named constants in cn specs

[yav]

It is common to use #define to name various constants in C, but it looks like these cannot be referenced in CN specifications. I am guessing that this happens because CN specs are comments and the preprocessor does not expand macros in comments.

Is there a known work around for this?

[yav]

One workaround that can be used at the moment is define a constant function, for example:

int c_INT_MAX() { return INT_MAX; }

[dc-mak]

Precisely as you identify, because of the C pre-processor and comments interaction. Perhaps one for the list of engineering-y/polish features to add. Anyways, below is the idiomatic way to do something like this.

/*@ function (i32) INT_MAX() @*/
int c_INT_MAX() /*@ cn_function INT_MAX @*/ { return INT_MAX; }

[dc-mak]

I am going to close this issue since the lack of explanation is noted in rems-project/cn-tutorial#4 and also it's not really something CN (or even Cerberus) can do much about.

Pre-processor shenanigans like macros are a tricky problem to solve in the general case (a Clang plugin would be required: https://github.com/rems-project/c-tree-carver/blob/main/cpp/src/reachability_analyzer.hpp) .

Perhaps a simple workaround would be to run a simple grep over a project, gather the constants in a temporary header file, and --include that file so that CN reads the definitions from it.