--- layout: fc_discuss_archives title: Message 111 from Frama-C-discuss on December 2009 ---
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