--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on April 2013 ---
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 ------------------------------------------------------------------------