# 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

**References**:**[Frama-c-discuss] casting from float to ulong and vice versa***From:*wintak2009 at gmail.com (Winny Takashi)

**[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***From:*wintak2009 at gmail.com (Winny Takashi)

- Prev by Date:
**[Frama-c-discuss] casting from float to ulong and vice versa** - Next by Date:
**[Frama-c-discuss] Problems with Window Installation of Frama-C** - Previous by thread:
**[Frama-c-discuss] casting from float to ulong and vice versa** - Next by thread:
**[Frama-c-discuss] Looking for paper describing Frama-C internals** - Index(es):