Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001683Frama-CPlug-in > wppublic2014-03-12 16:072016-01-26 08:52
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0001683: Number of discharged Qed goals counted multiple times
DescriptionHere are the last lines of output produced by WP when verifying the copy algorithm.
It appears that the Qed goals are counted several times.

[wp] Proved goals: 16 / 16
     Qed: 12 (2ms-8ms)
     Alt-Ergo: 11 (25ms-81ms) (70)
     cvc4: 1 (460ms-460ms)
Additional InformationIn fact, I am running Frama-C Neon...
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005025)
jens (reporter)
2014-04-03 15:16

 CVC4 results are also not correctly handled by -wp-report
(0005508)
correnson (manager)
2014-10-13 13:49

 Fix committed to master branch.
(0005921)
correnson (manager)
2015-05-20 15:34

 Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-03-12 16:07 jens New Issue
2014-03-12 16:07 jens Status new => assigned
2014-03-12 16:07 jens Assigned To => correnson
2014-04-03 15:16 jens Note Added: 0005025
2014-10-13 13:49 correnson Note Added: 0005508
2014-10-13 13:49 correnson Status assigned => resolved
2014-10-13 13:49 correnson Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
2015-05-20 15:34 correnson Note Added: 0005921
2015-05-20 15:34 correnson Status closed => resolved
2016-01-26 08:51 signoles Fixed in Version Frama-C Sodium => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker