View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001683 | Frama-C | Plug-in > wp | public | 2014-03-12 16:07 | 2016-01-26 08:52 | ||||
Reporter | jens | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Fluorine-20130601 | ||||||||
Target Version | Fixed in Version | Frama-C Magnesium | |||||||
Summary | 0001683: Number of discharged Qed goals counted multiple times | ||||||||
Description | Here 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 Information | In fact, I am running Frama-C Neon... | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
jens (reporter) 2014-04-03 15:16 |
CVC4 results are also not correctly handled by -wp-report |
correnson (manager) 2014-10-13 13:49 |
Fix committed to master branch. |
correnson (manager) 2015-05-20 15:34 |
Fix committed to master branch. |
![]() |
|||
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 |