Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001683Frama-CPlug-in > wppublic2016-01-26 08:52
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0005025

jens (reporter)

CVC4 results are also not correctly handled by -wp-report

~0005508

correnson (manager)

Fix committed to master branch.

~0005921

correnson (manager)

Fix committed to master branch.
+Notes

-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 Source_changeset_attached => framac master ba1a14eb
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 Source_changeset_attached => framac master 23c92dad
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
+Issue History