--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2010 ---
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