Frama-C Bug Tracking System - Frama-C | |||||
View Issue Details | |||||
ID | Project | Category | View Status | Date Submitted | Last Update |
0002237 | Frama-C | Plug-in > wp | public | 2016-06-30 15:31 | 2016-12-05 20:30 |
Reporter | Jochen | ||||
Assigned To | correnson | ||||
Priority | high | Severity | major | Reproducibility | always |
Status | closed | Resolution | fixed | ||
Platform | OS | OS Version | xubuntu | ||
Product Version | Frama-C Aluminium | ||||
Target Version | Fixed in Version | ||||
Summary | 0002237: Frama-C is unsound when employing both alt-ergo and cvc4 | ||||
Description | Running "frama-c -wp -wp-out out -wp-prover alt-ergo -wp-prover cvc4 bug.c" on the attached file "bug.c" proves both lemmas, although they are both obviously false. A look at file "lemma_Two_Alt-Ergo.mlw" shows that Alt-ergo proved in fact One==>Two, while a look at file "Axiomatic.why" indicates that cvc4 proved in fact Two==>One. Apparently, the order of lemmas is reversed when piping through "why" - the output generated for coq amounts to "prove One" and "prove One==>Two", similar to that for Alt-ergo. The problem disappeared when the type of the bound variable "x" was changed to "integer". | ||||
Steps To Reproduce | |||||
Additional Information | |||||
Tags | No tags attached. | ||||
Relationships | |||||
Attached Files | ![]() https://bts.frama-c.com/file_download.php?file_id=1105&type=bug ![]() https://bts.frama-c.com/file_download.php?file_id=1106&type=bug ![]() https://bts.frama-c.com/file_download.php?file_id=1107&type=bug ![]() https://bts.frama-c.com/file_download.php?file_id=1108&type=bug | ||||
Issue History | |||||
Date Modified | Username | Field | Change | ||
2016-06-30 15:31 | Jochen | New Issue | |||
2016-06-30 15:31 | Jochen | Status | new => assigned | ||
2016-06-30 15:31 | Jochen | Assigned To | => correnson | ||
2016-06-30 15:31 | Jochen | File Added: bug.c | |||
2016-06-30 15:32 | Jochen | File Added: lemma_Two_Alt-Ergo.mlw | |||
2016-06-30 15:32 | Jochen | File Added: Axiomatic.why | |||
2016-06-30 15:35 | Jochen | Note Added: 0006215 | |||
2016-06-30 19:11 | virgile | Note Added: 0006216 | |||
2016-07-01 10:59 | yakobowski | Note Added: 0006217 | |||
2016-07-01 10:59 | yakobowski | Priority | normal => high | ||
2016-07-04 09:54 | correnson | Status | assigned => resolved | ||
2016-07-04 09:54 | correnson | Resolution | open => fixed | ||
2016-07-04 09:54 | correnson | File Added: 0001-WP-Fix-definition-order.patch | |||
2016-12-05 20:30 | yakobowski | Status | resolved => closed | ||
2016-12-05 20:30 | yakobowski | Note Added: 0006306 |
Notes | |||||
|
|||||
|
|
||||
|
|||||
|
|
||||
|
|||||
|
|
||||
|
|||||
|
|