Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] casting from float to ulong and vice versa
  • From: wintak2009 at gmail.com (Winny Takashi)
  • Date: Thu, 16 Sep 2010 21:18:06 +0200
Hello there!

I'm trying to use Frama-c to analyze simple C functions using floats and
unsigned long together.
for instance:
//@ requires 0.05 <= a <= 5.0;
unsigned long cnv1(float a) {
unsigned long x;
x = (unsigned long)*((unsigned long *)(& a));
x = (*(unsigned long *)(&x)) & 2UL;
return x;
}
analyzed with frama-c -val, the returned value is [--;--].
this means infinity, it doesn't? is there smthing to do to get more precise
results, or is it out of scope?

Best,
WT
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100916/4c3ee907/attachment.htm>