Frama-C Bug Tracking System - Frama-C
View Issue Details
0002453Frama-CPlug-in > wppublic2019-06-14 13:202019-07-05 11:41
jens 
bobot 
normalmajoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C 19-Potassium 
0002453: number of generated files in Frama-C 18 vs 19. beta(2)
This entry references issue
    https://github.com/Frama-C/Frama-C-snapshot/issues/21 [^]
in order to be able to easily add files.
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.
No tags attached.
c rc.c (42,718) 2019-06-14 13:20
https://bts.frama-c.com/file_download.php?file_id=1316&type=bug
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

Notes
(0006785)
bobot   
2019-06-14 14:03   
The file names changed and they are perhaps not uniq anymore.
(0006786)
correnson   
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.
(0006787)
jens   
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.
(0006788)
bobot   
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 ;).)
(0006789)
jens   
2019-06-14 16:18   
Thanks for the clarification and the hints towards "-report"
(0006804)
jens   
2019-06-26 11:52   
It looks like the issue os not present in the final release of Frama-C 19.0
(0006805)
bobot   
2019-06-26 15:37   
Yes it has been fixed, thanks to your report!