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

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