Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002293Frama-CPlug-in > wppublic2017-03-16 17:212017-03-16 18:45
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C Silicon 
Target VersionFixed in Version 
Summary0002293: Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4
DescriptionI ran "frama-c -wp -wp-prover cvc4 -wp-prover alt-ergo -wp-prop bar gcd.c" and observed the input file "lemma_bar_Alt-Ergo.mlw" and "why_4e8b6a_Axiomatic-T-Q_bar.smt2" to Alt-ergo and Cvc4, respectively.

The former file contains as assumptions the lemmas "bar1" and "divisor1" (side remark: note the reversed order, compared to the Acsl source), which is ok.
However, the latter file contains as assumption just lemma "X", which imho is wrong.
In any case, the assumption sets given to Alt-ergo and Cvc4 should agree.

The problem might be a remainder of issue 0002237, which is meanwhile closed.
TagsNo tags attached.
Attached Filesc file icon gcd.c [^] (1,611 bytes) 2017-03-16 17:21 [Show Content]
? file icon lemma_bar_Alt-Ergo.mlw [^] (17,326 bytes) 2017-03-16 17:21
? file icon why_4e8b6a_Axiomatic-T-Q_bar.smt2 [^] (8,277 bytes) 2017-03-16 17:21

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-03-16 17:21 Jochen New Issue
2017-03-16 17:21 Jochen Status new => assigned
2017-03-16 17:21 Jochen Assigned To => correnson
2017-03-16 17:21 Jochen File Added: gcd.c
2017-03-16 17:21 Jochen File Added: lemma_bar_Alt-Ergo.mlw
2017-03-16 17:21 Jochen File Added: why_4e8b6a_Axiomatic-T-Q_bar.smt2


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker