--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



On Sat, Sep 18, 2010 at 10:29 PM, Winny Takashi <wintak2009 at gmail.com> wrote:

> however problem seems to occur on biwise "|" too:

Well, it would too, wouldn't it?
In general terms, bitwise & mixes better with interval+congruence
representation of sets of values than bitwise |. When one of the
operands is unknown and the other is known precisely, in the case of
bitwise &, it is possible to know that some output bits are zero,
which limits the values of the output in a way that can be expressed
as a reduction of the values of the interval bounds. In the case of
bitwise |, it is only possible to know that some output bits are one,
which does not result in additional information on the bounds of the
output interval in the case of an unsigned operation as in your
program.

> //@ requires 0.05 <= a <= 5.0;
> unsigned long cnv2(float a)
> {
> ??? unsigned long x;
> x = (unsigned long)*((unsigned long *)(& a));
> Frama_C_show_each_x1(x);
> //@ requires 0.1 <= x <= 3.0;
> Frama_C_show_each_x2(x);

I get:

[value] Called Frama_C_show_each_x2([0.1 .. 5.])

with the development version here. This is indeed strange. Perhaps we
have not considered the full ramifications of the presence of implicit
casts from integer to real in ACSL in the value analysis. We will look
at this.

In any case, you should use "//@ assert" for a property in a specific
point inside a function. //@ requires only works by accident, so to
speak, because the annotation is considered as a statement contract on
the statement Frama_C_show_each_x2(x);

> return value is in --;--
> even if frama_c_show_x3 seems more precise.

That part is easy: [--..--] is not really more precise for an unsigned
long than [0..4294967295], because the latter represents all possible
values for a 32-bit unsigned long. The two representations are
converted back and forth in various phases of the analysis. The
conversion to [0..4294967295] is made for the purpose of precision,
the conversion to [--..--] is made for the purpose of compacity of the
memory representation of the results and readability.

You may encounter one or the other depending on the way you inspect
the same value. They mean the same thing.

Pascal