--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin



Hi,

On Mon, May 9, 2016 at 5:51 PM, Maurice Bremond <Maurice.Bremond at inria.fr>
wrote:

> with N=1093:
>
> [...]
> x ∈ [-1000000. .. 1000000.]
> x0 ∈ [-0. .. 1e+12]
>
> N=1094:
>
> [...]
> x ∈ [-1000000. .. 1000000.]
> x0 ∈ [0. .. 1e+12]
>
>
> I did not look at the assertion... It becomes valid here for N=1 !
>
> I just thought that if x0 is only printed as >= -0 in the output of
> value analysis, it means that there is a possibility that it is >= a
> small negative value that has been rounded to zero and then x0 >= 0 may
> not hold, so it is not necessary to check the assertion.
>
>
Thanks for the clarification! I did not notice that -0. was disappearing
from the possible values with N>=1094.

The assertion is proven for N = 1 because the interval for x is
symmetrical: the first subdivision results in [-1e6 .. +0] and [succ(+0) ..
1e6], whose images are in [-0. .. 1e12]. The next 1093 subdivisions are
useful only to refine the intervals so that we get [+0. .. +0.] on the one
hand, and a strictly negative interval on the other hand.

By the way, to avoid problems with the display of floating-point values,
you can use options -float-hex or -float-normal.


> I only try to see the disparition of the -0 bound with
> the increase of N.
>
> For:
>   double x0 = (x-0.1)*(x-0.1);
>
> the -0 bound seems to never disappear (in fact the value plugin returns
> quickly even if N is very high)
>
> And the assertion becomes valid for N=75.
>
>
Indeed. It seems that the code that subdivides an interval in two is a bit
conservative. It will not split two consecutive floats [u..v] into [u..u]
and [v..v]. Thanks for pointing this out!


-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160510/b76c8e57/attachment.html>