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>
- Follow-Ups:
- [Frama-c-discuss] casting from float to ulong and vice versa
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] casting from float to ulong and vice versa
- Prev by Date: [Frama-c-discuss] GUI - Opening a file (Windows XP)
- Next by Date: [Frama-c-discuss] casting from float to ulong and vice versa
- Previous by thread: [Frama-c-discuss] GUI - Opening a file (Windows XP)
- Next by thread: [Frama-c-discuss] casting from float to ulong and vice versa
- Index(es):