--- layout: fc_discuss_archives title: Message 15 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



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