--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] casting from float to ulong and vice versa



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>