--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on April 2013 ---
Hi, Which version of Frama-C/Wp are you using ? Latest release Fluorine leads to : [wp] 3 goals scheduled [wp] [Qed] Goal typed_f_assign : Valid [wp] [Qed] Goal typed_f_B_post : Valid [wp] [Alt-Ergo] Goal typed_f_A_post : Valid (21ms) (11) By the way, resources for reasoning over machine integers are limited in WP for automated provers. The reason is that reasoning with modulus generally drives alt-ergo and such into larger research space. You have all the necessary axiomatizations in Coq, however. A common practice is to insert assertions and lemmas to be proven in Coq. Example : assumes the following code, where you know that "c" potentially overflows. { unsigned char c; ... c++; ... } You may add the following lemma : /*@ lemma uint8_incr : \forall integer x ; (unsigned char) (x-256) == (unsigned char) x ; */ Prove it in CoqIde : Proof. intros. unfold to_uint8. unfold to_range. simpl. replace (x_0 - 0) -> x_0 by auto with zarith. replace (x_0 - 256 - 0) -> (x_0 + (-1) * 256) by ring. symmetry. apply Z_mod_plus_full. Qed. And now, Alt-Ergo and such can use this fact. L. Le 26 avr. 2013 ? 17:20, Damien Karkinsky a ?crit : > Hello, > > I had a simple function with the following contract: > > #include<stdint.h> > > uint16_t x; > > /*@ > assigns x; > > behavior A: > assumes x < 65535; > ensures x == \old(x) + 1; > > behavior B: > assumes x == 65535; > ensures x == 0; > */ > void f(); > > > void f(){ > ++x; > } > > void main(){ > f(); > } > > I cannot verify the post condition for behaviour B. WP states > Goal store_f_B_post_2: > forall x_0:int. > is_uint16(x_0) -> > (x_0 = 65535) -> > (let x_1 = as_uint16(65536) in > (x_1 = 0)) > > I suppose as_uint16(65536) = 0 is not derived to be the case. > > Would any one care to comment? Is that a bug? > > Thank you and all the best > Damien > > -- > ------------------------------------------------------------------------ > > Dr. Damien Karkinsky > > Safety-Critical Systems Consultant > > Adelard LLP. (www.adelard.com) > > Exmouth House, 3-11 Pine Street, London, EC1R 0JH > > tel: +44(0)20-7832-5854 mob: +44(0)779-568-1233 > > ------------------------------------------------------------------------ > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss