--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving stack axioms with jessie



Le mar. 17 ao?t 2010 13:42:28 CEST,
"Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit :

> > Could you specify which automated prover(s) prove the false
> > post-condition of equal_pop? When I run "frama-c-Jessie -jessie
> > equal_pop.c" with Boron I get timeouts from alt-ergo 0.91 for "0==1"
> > and for "Equal(s,t)".
> 
> It is Simplify that proves the false one in this example. The other provers return a time-out.
> 

I have the same behavior as Pascal (no proof for Equal(s,t) and 0==1 in
equal_pop) for alt-ergo 0.91, Simplify 1.5.4 and Z3 2.0 (Frama-C Boron
and Why 2.26).
Just in case, when you ran your experiment with equal_pop, you had the
ensures 0==1 commented out in the spec of pop itself, as it is in the
archive, right? Otherwise, the issue lies there.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile