|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002293||Frama-C||Plug-in > wp||public||2017-03-16 17:21||2017-03-16 18:45|
|Assigned To||correnson|| |
|Product Version||Frama-C 14-Silicon|| |
|Target Version||Fixed in Version|| |
|Summary||0002293: Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4|
|Description||I 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 #2237, which is meanwhile closed.|
|Tags||No tags attached.|
|Attached Files|| gcd.c [^] (1,611 bytes) 2017-03-16 17:21 [Show Content]
lemma_bar_Alt-Ergo.mlw [^] (17,326 bytes) 2017-03-16 17:21
why_4e8b6a_Axiomatic-T-Q_bar.smt2 [^] (8,277 bytes) 2017-03-16 17:21