--- layout: fc_discuss_archives title: Message 112 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proof conditions with simple pointer assignment



Hello,

Le ven. 11 d?c. 2009 16:44:20 CET,
Damien Karkinsky <dak at adelard.com> a ?crit :

> /*@ requries \valid(p);
>    @ assigns *p;
>    @ ensures *p == 1;
> */
> void f(int *p)
> {
>     *p = 1;
> }

> The conditions is not discharged although axiom select_store_eq seems
> quite sufficient to discharge it. Is integer_of_int32 somehow getting in
> the way?

Which prover are you using? alt-ergo 0.9 seems indeed to have some
difficulties, but Simplify 1.5.4 and z3 2.0 succeed on all obligations.

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile