workaround for coq-8.5.1 issue?
ID0002233: This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002233 | Frama-C | Plug-in > wp | public | 2016-06-16 | 2016-12-05 |
| Reporter | Jochen | Assigned To | correnson | Resolution | no change required |
| Priority | none | Severity | feature | Reproducibility | always |
| Platform | Aluminium-20160501 | OS | xubuntu16.04 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
We ran the command
frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.con the attached file "adi.c", using the attached Coq-script "wp0.script".
The goal isn't proven, and when manually starting the Coq Ide, it complains:
Error: The reference Q_UnchangedSection was not found in the currentenvironment.
However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).
For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.
Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.