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.
|ID0002453||Frama-C||Plug-in > wp||public||2019-06-14||2019-07-05|
|Product Version||Frama-C GIT, precise the release id||Target Version||-||Fixed in Version||Frama-C 19-Potassium|
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.