number of generated files in Frama-C 18 vs 19. beta(2)
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.