Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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