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.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 environment. 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. ## Attachments - [adi.c](/uploads/c4c8150d300c94e05ae4078a54bb0388/adi.c) - [wp0.script](/uploads/7a7bb805cc9c8332faccefd8ebe42e5d/wp0.script) - [Axiomatic.v](/uploads/9ab08c5dc84284dc5f8412c7ddc95f09/Axiomatic.v) - [lemma_AdjacentDifferenceInverse_Coq.v](/uploads/d61593407465c9df0f749dc04240e6ea/lemma_AdjacentDifferenceInverse_Coq.v) - [adi.script](/uploads/9ab0f4bd54640d060c2292833e1bcd01/adi.script)