--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2016 ---
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>