--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on September 2010 ---
Hello, Thanks for your answer. however problem seems to occur on biwise "|" too: //@ requires 0.05 <= a <= 5.0; unsigned long cnv2(float a) { unsigned long x; x = (unsigned long)*((unsigned long *)(& a)); Frama_C_show_each_x1(x); //@ requires 0.1 <= x <= 3.0; Frama_C_show_each_x2(x); x = (*(unsigned long *)(&x)) | 2UL; Frama_C_show_each_x3(x); return x; } I've got many questions on what was displayed on stdout, but mainly: return value is in --;-- even if frama_c_show_x3 seems more precise. Best, WT -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100918/41cc2a63/attachment.htm>