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: Sun, 19 Sep 2010 00:20:04 +0200
  • In-reply-to: <AANLkTi=sVBXjPzrJiUvALZJEsSWiC=A5aJ60r7G+bz99@mail.gmail.com>
  • References: <AANLkTikM4u=PpSpi4vzmAHkHr_+aFg3C4wYb1YJnjV5Y@mail.gmail.com> <AANLkTi=aCpQd-QAJCNZMD8RPC2nrPGa11tRLb5CDYJM+@mail.gmail.com> <AANLkTi=sVBXjPzrJiUvALZJEsSWiC=A5aJ60r7G+bz99@mail.gmail.com>
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