Introduce option warn with options post | early | never

[michael-schwarz]

The behavior is as follows:

• default: Warn in verifying phase, run verification regardless of verify, do not report problems if verify is false
• early: Same as above except that during solving warnings are already produced
• none: Do not produce warnings. Verification is run iff verify is true

Also the unused option ana.warnings was removed, and the config for incremental was fixed.

warn set to early replaces dbg.earlywarn.

Closes #88. References #28

[sim642]

I didn't look at anything else yet, but the value default seems weird, because then you have the option's default value be default, which isn't descriptive at all. But I don't know what the ideal alternative would be either. Maybe solved as in it's reporting them on the solved state, or post as in post-solving?

Maybe we need a new name for the verification phase, if it can be used either for verifying the solution or for reporting warnings.

[michael-schwarz]

post as in post-solving?

I renamed it thus.

Maybe we need a new name for the verification phase, if it can be used either for verifying the solution or for reporting warnings.

I would want to stick with verify as that also makes sense in purely the fixpoint sense, especially since verify is likely not set to false too often, so it is very seldom that is used not only for verifying and only for warning.