--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on September 2010 ---
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>