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