--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on September 2010 ---
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