Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002453Frama-CPlug-in > wppublic2019-06-14 13:202019-07-05 11:41
Reporterjens 
Assigned Tobobot 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 https://github.com/Frama-C/Frama-C-snapshot/issues/21 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 file icon rc.c [^] (42,718 bytes) 2019-06-14 13:20 [Show Content]

- Relationships

-  Notes
(0006785)
bobot (administrator)
2019-06-14 14:03

The file names changed and they are perhaps not uniq anymore.
(0006786)
correnson (manager)
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 (reporter)
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 (administrator)
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 (reporter)
2019-06-14 16:18

Thanks for the clarification and the hints towards "-report"
(0006804)
jens (reporter)
2019-06-26 11:52

It looks like the issue os not present in the final release of Frama-C 19.0
(0006805)
bobot (administrator)
2019-06-26 15:37

Yes it has been fixed, thanks to your report!

- Issue History
Date Modified Username Field Change
2019-06-14 13:20 jens New Issue
2019-06-14 13:20 jens Status new => assigned
2019-06-14 13:20 jens Assigned To => correnson
2019-06-14 13:20 jens File Added: rc.c
2019-06-14 14:03 bobot Note Added: 0006785
2019-06-14 14:06 correnson Note Added: 0006786
2019-06-14 14:10 jens Note Added: 0006787
2019-06-14 15:27 bobot Note Added: 0006788
2019-06-14 16:18 jens Note Added: 0006789
2019-06-26 11:52 jens Note Added: 0006804
2019-06-26 15:37 bobot Note Added: 0006805
2019-06-26 15:38 bobot Status assigned => resolved
2019-06-26 15:38 bobot Fixed in Version => Frama-C 19-Potassium
2019-06-26 15:38 bobot Resolution open => fixed
2019-06-26 15:38 bobot Assigned To correnson => bobot
2019-07-05 11:41 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker