--- layout: fc_discuss_archives title: Message 7 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



Hello,

> 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.

(But by running these kind of experiments I also saw Alt-Ergo prove such a
false postcondition in an analogue example of a Queue.) 

Thanks for the other hint,
I'm going to try what you suggested.

Regards,
Kerstin

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 2951 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100817/244cb892/attachment.bin>