Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002011Frama-CPlug-in > wppublic2014-12-02 12:132014-12-02 12:13
Reporterjzinzind 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformLinuxOSUbuntuOS Version14.04
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0002011: Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas
DescriptionOne can prove the following : /*@ axiomatic Bla{ predicate Pred(integer x); lemma lemme1: \forall integer x; Pred(x) ; lemma lemme2: \forall integer x; Pred(x) ; } */ using native alt-ergo and an SMT solver from the Why3 plateform. Native alt-ergo and the why3 based SMT solver do not parse the lemmas in the same order. So one can prove lemma2 assuming lemma1, the other can prove lemma1 because it assumes lemma2, and evenntually the whole axiomatic is proven. This is very problematic and confusing whenever several different SMT solvers are used.
Steps To ReproduceHave SMT solvers imported from why3 0.83, Frama C Neon and the WP plugin
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-12-02 12:13 jzinzind New Issue
2014-12-02 12:13 jzinzind Status new => assigned
2014-12-02 12:13 jzinzind Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker