--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on September 2010 ---
Hello, On Thu, Sep 16, 2010 at 9:18 PM, Winny Takashi <wintak2009 at gmail.com> wrote: > 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? Well, something could be done quickly to recognize that the result of an unknown value & 2UL is {0 ; 2; }. In fact, this is already handled for the most part, there is just a quirk (that your code exhibits) in that the value of x in the middle of the function is not an unknown value, but known to be exactly the bits of a floating-point value between 0.05 and 5. You can see that by inserting Frama_C_show_each_x(x); between the two assignments to x. If x was properly unknown, for instance by changing the first assignment to: x = 1 + (unsigned long)*((unsigned long *)(& a)); then the result would be more precise for the end value of x: x ? {0; 1; 2; } That part is a definite bug: more precise values in should always mean more precise values out. It's probably a single-line fix too, so if you are compiling Frama-C from sources, I can provide a patch. You are probably more interested in the (unsigned long)*((unsigned long *)(& a)) part though. The first reason that is not a single-line fix is that your program is using floats, when only doubles are currently supported. Floats are treated as if they were doubles that magically fit inside 32 bits. No-one has complained too loudly so far (it is documented that the handling of floating-point computations have limitations), but if you are going to convert the bits of a float to the bits of a long you will definitely notice. Now, if your program was manipulating doubles and long long ints, there would be something to do, because intervals of doubles of the same sign do in fact map well to intervals of 64-bit integers. So in short: - & 2UL: already treated, but quirky, fixed soon in the development version and you can expect it will work in the next release; - *(unsigned long long *)&a where a is a double: a short time of work; - handling floats precisely: something that you can only speed up by being in a collaboration with us and weighting in on the importance of this feature compared to the thousand of other features that are also still unimplemented. To be clear, the eventual goal is to accept your program as it is and to treat it precisely. It is definitely "in scope". The fact that it is not treated as is is just a bug that will take a long time to be fixed. Pascal