Specification cannot resolve value for C "define" macro

[ArmborstL]

The C code below uses a #define macro, and uses the defined value in code as well as in spec.

#define DBL_MAX 1E+37

//@ requires a < DBL_MAX;
int main(int a) {
    a = DBL_MAX;
}

On this file, VerCors gives the error "Could not find local named DBL_MAX." for the usage in the precondition. If I comment the precondition (but leave the code usage in), then VerCors verifies successfully (i.e. it can resolve the value for the code usage).

VerCors should be able to resolve define values also in specifications.

My guess is that we use the "normal" clang pre-processor to resolve macros. There, specifications look just like comments, so it does not replace those macro usages. Thus, VerCors parses a file where the code usages have been replaced, and thus cause no issue, while the spec usages are still there, and cause issues.
I'm not sure how to best resolve this. Maybe the pre-processor can be instructed to also replace in comments?

[pieter-bos]

I agree that this should work: our view is that in contract-mode you can write all C expressions as normal, and this should include macros. There's no option to do this in clang/gcc as far as I can tell.

The way we use clang (or equivalently any gcc-compatible compiler) has a few drawbacks:

• It needs a lot of convincing not to include any system include files, so we can supply our (specified) own
• Origins are a bit harder to construct, because we need to reconstruct file positions via line markers

It might be time that we ship our own preprocessor, I see two concrete options:

• Bob recently mentioned that http://shevek.github.io/jcpp/docs/javadoc/ exists, I don't know if it is flexible enough to do what you want here
• We can implement our own preprocessor. I don't think that is actually too difficult: the standard spends 18 pages on it.

I think both of these have the benefit that we start from a blank slate (e.g. in terms of system includes, pre-defined platform-specific macros, and so on). If we implement our own, origins can also be a lot better, since we can get token granularity position reporting instead of simple line based reporting. We might even be able to get away with just reporting stuff at the C source.

[pieter-bos]

I gave doing our own preprocessor a go, some things I noticed:

• Conditional directives (#if and so on) tacitly take an expression as a condition that just refers to the regular expression grammar, so we would need to be able to evaluate those. We might be able to just use the ANTLR grammar to parse them. I think VerCors should eventually have an opinion on stuff like input/execution character set, integer width, etc. regardless.
• We can make origins very nice, keeping track of how things are macro-expanded along the way.