| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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. |
| 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 |