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

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