Suggest to supply values of global consts to provers
ID0001179: This issue was created automatically from Mantis Issue 1179. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001179 | Frama-C | Plug-in > wp | public | 2012-05-10 | 2016-06-21 |
| Reporter | Jochen | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Aluminium |
Description :
Wp/Simplify couldn't prove behavior-disjointness in line 5 of the attached program. The reason is that no information about the fixed values of c1 and c2 appears in the proof obligation. If the declarations in line 1-2 are replaced by #define-s, the proof is trivially found.
I suggest to replace in the proof obligation each const variable by its value, if it is known at compile time. The latter restriction is satisfied for all variables visible in contracts (as opposed e.g. to asserts).
Preferring C constants to macros is considered good software engineering practice; it shouldn't be discouraged by Frama-C/Wp.