--- layout: fc_discuss_archives title: Message 117 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,
Just from an ACSL point of view, the proof of the "assigns"
and "ensures" clauses of your spec requires locations "p"
and "*p" to be \separated.
Patrick Baudin.
-- 

Patrick Baudin,
CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

> Hello,
>
> Consider the following spec,
>
> /*@ requries \valid(p);
>    @ assigns *p;
>    @ ensures *p == 1;
> */
> void f(int *p)
> {
>     *p = 1;
> }
>
> This generates the proof condition (in consice terms)
> H2:  integer_of_int32(result) = 1
> int_P_int_M_p_1_0: int(int_P, int32) memory
> H3: int_P_int_M_p_1_0 = store(int_P_int_M_p_1, p, result)
> -------------------------
> integer_of_int32(select (int_P_int_M_p_1_0, 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?
>
> Thank you
> Damien
>