Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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".
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (99 bytes) 2016-06-30 15:31 [Show Content]
? file icon lemma_Two_Alt-Ergo.mlw [^] (22,497 bytes) 2016-06-30 15:32
? file icon Axiomatic.why [^] (545 bytes) 2016-06-30 15:32
patch file icon 0001-WP-Fix-definition-order.patch [^] (2,387 bytes) 2016-07-04 09:54 [Show Content]

- Relationships

-  Notes
(0006215)
Jochen (reporter)
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 (developer)
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 (manager)
2016-07-01 10:59

Bumping the severity because of the unsoundness.
(0006306)
yakobowski (manager)
2016-12-05 20:30

Fixed in Frama-C Silicon.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker