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] 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>