workaround for coq-8.5.1 issue?
ID0002233: This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.
|ID0002233||Frama-C||Plug-in > wp||public||2016-06-16||2016-12-05|
|Reporter||Jochen||Assigned To||correnson||Resolution||no change required|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.c
on 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 current
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.