--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on May 2016 ---
Hello, >This setting (1094) seems a bit high for such a simple formula. Out of curiosity, what were the possible values >for x? I made this test for x â [-1e6, 1e6] #include <__fc_builtin.h> int main() { double x = Frama_C_double_interval(-1e6, +1e6); double x0 = x*x; /*@ assert x0 >= 0.; */ return 0; } frama-c -val t.c -val-subdivide-non-linear N But I only checked the lower bound for x0 in the output of the value plugin, it is -0 until N=1094 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. >Again, this is a bit strange. I'm able to analyse the following program and prove that r >= -0. using >-val-subdivide-non-linear 1080. You may obtain different results with different bounds for x, because the >subdivision strategy depends on the initial interval. However, there should be no need to go to extreme values >such as 99999. 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. Maurice