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

the specifications written at FIRST are always clear and enjoyable to read.

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

Also, the remaining specification of equal_pop, for instance the
postcondition *x==*y, is not true if there is aliasing between s and
t. And when you start verifying function push, aliasing between s->c
and t->c will become a possible issue, too. I am pretty sure that
Jessie's default separation policy is to assume this absence of
aliasing, so that should be fine.

Pascal