applicability of Coq proof script depends on order of include files
ID0002282: This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002282 | Frama-C | Plug-in > wp | public | 2017-02-16 | 2017-02-16 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Silicon-20161101 | OS | xubuntu | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
We run "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prop HeapMaximum -wp-prover coq make_heap_cpp.c" on the attached files. In the current form, the Coq proof script "wp0.script" works fine and proved the lemma "HeapMaximum" from file "make_heap_cpp.c".
However, when that lemma is moved after the "axiomatic Count", which is completely unrelated, the same command doesn't work any longer. Using "-wp-out" shows that both versions differ in the location where lemma "HeapBounds" is available in Coq; this make it necessary to change the names used in the proof.
The problem originated from lemma "HeapMaximum" being used for the verification of two different function contracts. For software engineering reasons, the order of #include files was different (since different files were preferred to be included in the ".c", rather than already in the ".h" file). This resulted in "lemma HeapMaximum" appearing before and after an "axiomatic", making "wp0.script" work and not work, respectively.