Frama-C Bug Tracking System - Frama-C
View Issue Details
0002453Frama-CPlug-in > wppublic2019-06-14 13:202019-07-05 11:41
Assigned Tobobot 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C 19-Potassium 
Summary0002453: number of generated files in Frama-C 18 vs 19. beta(2)
DescriptionThis entry references issue
in order to be able to easily add files.
Steps To ReproduceRun 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.
TagsNo tags attached.
Attached Filesc rc.c (42,718) 2019-06-14 13:20

2019-06-14 14:03   
The file names changed and they are perhaps not uniq anymore.
2019-06-14 14:06   
The files are only generated when Qed did not solve the goals ; what happened is that v19 is much better than v18 at solving with Qed :-)

To get stable results, use the -wp-report option or, even better, the -report and -report-classify utilities.
2019-06-14 14:10   
I don't understand the last remark as both versions claim that 5 VC were successfully handled by Qed and the remaining 12 by Alt-Ergo. In other words, for this particular example, Qed is not better.
2019-06-14 15:27   
Yes there is really a regression, it will be fixed. (However using -report could still be a better idea than looking at the files present ;).)
2019-06-14 16:18   
Thanks for the clarification and the hints towards "-report"
2019-06-26 11:52   
It looks like the issue os not present in the final release of Frama-C 19.0
2019-06-26 15:37   
Yes it has been fixed, thanks to your report!

Issue History
2019-06-14 13:20jensNew Issue
2019-06-14 13:20jensStatusnew => assigned
2019-06-14 13:20jensAssigned To => correnson
2019-06-14 13:20jensFile Added: rc.c
2019-06-14 14:03bobotNote Added: 0006785
2019-06-14 14:06corrensonNote Added: 0006786
2019-06-14 14:10jensNote Added: 0006787
2019-06-14 15:27bobotNote Added: 0006788
2019-06-14 16:18jensNote Added: 0006789
2019-06-26 11:52jensNote Added: 0006804
2019-06-26 15:37bobotNote Added: 0006805
2019-06-26 15:38bobotStatusassigned => resolved
2019-06-26 15:38bobotFixed in Version => Frama-C 19-Potassium
2019-06-26 15:38bobotResolutionopen => fixed
2019-06-26 15:38bobotAssigned Tocorrenson => bobot
2019-07-05 11:41signolesStatusresolved => closed