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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 17 Sep 2010 02:42:58 +0200
  • In-reply-to: <AANLkTikM4u=PpSpi4vzmAHkHr_+aFg3C4wYb1YJnjV5Y@mail.gmail.com>
  • References: <AANLkTikM4u=PpSpi4vzmAHkHr_+aFg3C4wYb1YJnjV5Y@mail.gmail.com>
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