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