ID0002453: **This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002453 | Frama-C | Plug-in > wp | public | 2019-06-14 | 2019-07-05 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jens | **Assigned To** | bobot | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium | ### Description : This entry references issue https://github.com/Frama-C/Frama-C-snapshot/issues/21 in order to be able to easily add files. ### Steps To Reproduce : Run the command frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c on the attached files. As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo. However, Frama-C 18.0 generates 12 .mlw and .out files, respectively. Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively. The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo. ## Attachments - [rc.c](/uploads/12c6518483a56dad661d3ee7feabf59b/rc.c)