Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0002237Frama-CPlug-in > wppublic2016-06-30 15:312016-12-05 20:30
ReporterJochen 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Versionxubuntu
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002237: Frama-C is unsound when employing both alt-ergo and cvc4
DescriptionRunning "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
TagsNo tags attached.
Relationships
Attached Filesc bug.c (99) 2016-06-30 15:31
https://bts.frama-c.com/file_download.php?file_id=1105&type=bug
? lemma_Two_Alt-Ergo.mlw (22,497) 2016-06-30 15:32
https://bts.frama-c.com/file_download.php?file_id=1106&type=bug
? Axiomatic.why (545) 2016-06-30 15:32
https://bts.frama-c.com/file_download.php?file_id=1107&type=bug
patch 0001-WP-Fix-definition-order.patch (2,387) 2016-07-04 09:54
https://bts.frama-c.com/file_download.php?file_id=1108&type=bug
Issue History
Date ModifiedUsernameFieldChange
2016-06-30 15:31JochenNew Issue
2016-06-30 15:31JochenStatusnew => assigned
2016-06-30 15:31JochenAssigned To => correnson
2016-06-30 15:31JochenFile Added: bug.c
2016-06-30 15:32JochenFile Added: lemma_Two_Alt-Ergo.mlw
2016-06-30 15:32JochenFile Added: Axiomatic.why
2016-06-30 15:35JochenNote Added: 0006215
2016-06-30 19:11virgileNote Added: 0006216
2016-07-01 10:59yakobowskiNote Added: 0006217
2016-07-01 10:59yakobowskiPrioritynormal => high
2016-07-04 09:54corrensonStatusassigned => resolved
2016-07-04 09:54corrensonResolutionopen => fixed
2016-07-04 09:54corrensonFile Added: 0001-WP-Fix-definition-order.patch
2016-12-05 20:30yakobowskiStatusresolved => closed
2016-12-05 20:30yakobowskiNote Added: 0006306

Notes
(0006215)
Jochen   
2016-06-30 15:35   
The tool version are reported as follows:

frama-c --version --> Aluminium-20160501
why3 --version --> Why3 platform, version 0.87.0 ...
alt-ergo -version --> 0.99.1
cvc4 --version --> This is CVC4 version 1.4 ...
(0006216)
virgile   
2016-06-30 19:11   
The problem does not really disappear. It is just that for some unknown reason alt-ergo is not able to prove Two from One when we quantify over integer and not int. But there exists a trivial Coq proof for it (namely 'exact Q_one.'), and cvc4 is still able to prove One (using Two as hypothesis), closing the cycle again.
(0006217)
yakobowski   
2016-07-01 10:59   
Bumping the severity because of the unsoundness.
(0006306)
yakobowski   
2016-12-05 20:30   
Fixed in Frama-C Silicon.