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] Value Analysis - assertion, slevel and sqrt function

  • Subject: [Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Thu, 22 Nov 2012 21:13:12 -0200
Hi,

We have been working with Value Analysis Plugin (version Carbon) with a
real case study.

In the Frama-C Value Analysis plug-in 20110201 (Carbon), Section 7.1.2 Case
analysis, page 64, we saw the following example:

x = Frama_C_interval(-10,10);
//@assert x <= 0 || x >= 0 ;
y = x*x;

The example shown that if an assertion is a disjunction, then the reduction
of the state by the assertion may be computed independently for each
disjunct.

In our case study, the program calls the sqrt function 2 times with the
following parameters:
sqrt(a*a + b*b + c*c);

Our doubt is how to define the argument of the option slevel, i.e., the
number of times that is necessary to deal with the assertion.

It has worked with the minimum value equal 32:
>> frama-c -val sqrt.c /usr/share/frama-c/builtin.c
/usr/share/frama-c/math.c -slevel 32

We have 2 doubts:
1- how to define the correct value to the argument of the option slevel;
2- the program called the function Frama_C_show_each to verify the value of
the variables, but we have observed that the function is called several
times. Why does it occur?

The source code and the log are attached bellow.

Best Regards,
Rovedy, Nanci, Luciana

void main (void){
   float aux, tmp, a, b, c, d, e, f;

   a= Frama_C_float_interval(83.9759990008, 12666.8879961);
   b= Frama_C_float_interval(-2099.83521856, 2094.46878047);
   c= Frama_C_float_interval(-6276.20023952, 6306.71175755);
//@assert a <= 0 || a >= 0 ;
//@assert b <= 0 || b >= 0 ;
//@assert c <= 0 || c >= 0 ;
aux = a*a;
Frama_C_show_each_aa(aux);
aux = b*b;
Frama_C_show_each_bb(aux);
aux = c*c;
Frama_C_show_each_cc(aux);

aux = (a*a) + (b*b) + (c*c);
Frama_C_show_each_aux(aux);
tmp = sqrt(aux);

   d= Frama_C_float_interval(-61847529062.4, 61847529033.6);
   e= Frama_C_float_interval(-20615843020.8, 20615843011.2);
   f= Frama_C_float_interval(-61847529062.4, 61847529033.6);
//@assert d <= 0 || d >= 0 ;
//@assert e <= 0 || e >= 0 ;
//@assert f <= 0 || f >= 0 ;
aux = d*d;
Frama_C_show_each_dd(aux);
aux = e*e;
Frama_C_show_each_ee(aux);
aux = f*f;
Frama_C_show_each_ff(aux);

aux = (d*d) + (e*e) + (f*f);
Frama_C_show_each_aux(aux);
tmp = sqrt(aux);

}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121122/d2e5df3a/attachment-0001.html>
-------------- next part --------------
[kernel] preprocessing with "gcc -C -E -I.  sqrt.c"
[kernel] preprocessing with "gcc -C -E -I.  /usr/share/frama-c/builtin.c"
[kernel] preprocessing with "gcc -C -E -I.  /usr/share/frama-c/math.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        Frama_C_entropy_source ? {0; }
[value] float support is experimental
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:16.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:17.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:18.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
sqrt.c:19:[value] Assertion got status valid.
sqrt.c:20:[value] Assertion got status valid.
sqrt.c:21:[value] Assertion got status valid.
sqrt.c:22:[value] assigning non deterministic value for the first time
[value] Called Frama_C_show_each_aa([7051.96840818 .. 160450051.506])
[value] Called Frama_C_show_each_aa([7051.96840818 .. 160450051.506])
[value] Called Frama_C_show_each_aa([7051.96840818 .. 160450051.506])
[value] Called Frama_C_show_each_aa([7051.96840818 .. 160450051.506])
[value] Called Frama_C_show_each_bb([-0. .. 4409307.9451])
[value] Called Frama_C_show_each_bb([-0. .. 4409307.9451])
[value] Called Frama_C_show_each_bb([-0. .. 4386799.47236])
[value] Called Frama_C_show_each_bb([-0. .. 4386799.47236])
[value] Called Frama_C_show_each_cc([-0. .. 39390689.4466])
[value] Called Frama_C_show_each_cc([-0. .. 39774613.1928])
[value] Called Frama_C_show_each_cc([-0. .. 39390689.4466])
[value] Called Frama_C_show_each_cc([-0. .. 39774613.1928])
[value] Called Frama_C_show_each_aux([7051.96840818 .. 204250048.897])
[value] Called Frama_C_show_each_aux([7051.96840818 .. 204633972.644])
[value] Called Frama_C_show_each_aux([7051.96840818 .. 204227540.425])
[value] Called Frama_C_show_each_aux([7051.96840818 .. 204611464.171])
[value] computing for function sqrt <-main.
        Called from sqrt.c:31.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:31.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:31.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:31.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:33.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:33.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:33.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:33.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:34.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:34.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:34.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:34.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:35.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:35.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:35.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <-main.
        Called from sqrt.c:35.
[value] computing for function Frama_C_update_entropy <-Frama_C_float_interval <-main.
        Called from /usr/share/frama-c/builtin.c:55.
[value] Done for function Frama_C_update_entropy
[value] Recording results for Frama_C_float_interval
[value] Done for function Frama_C_float_interval
sqrt.c:36:[value] Assertion got status valid.
sqrt.c:37:[value] Assertion got status valid.
sqrt.c:38:[value] Assertion got status valid.
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_dd([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983458e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ee([-0. .. 4.25012983062e+20])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511685112e+21])
[value] Called Frama_C_show_each_ff([-0. .. 3.82511684756e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668571e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668531e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667858e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667819e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668571e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668531e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667858e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667819e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668571e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668531e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667858e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667819e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668571e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668531e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668214e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667858e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524668175e+21])
[value] Called Frama_C_show_each_aux([-0. .. 8.07524667819e+21])
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] computing for function sqrt <-main.
        Called from sqrt.c:48.
[value] Recording results for sqrt
[value] Done for function sqrt
[value] Recording results for main
[value] done for function main
[from] Computing for function Frama_C_float_interval
[from] Computing for function Frama_C_update_entropy <-Frama_C_float_interval
[from] Done for function Frama_C_update_entropy
[dominators] computing (post) for function Frama_C_float_interval
[dominators] done for function Frama_C_float_interval
[from] Done for function Frama_C_float_interval
[from] Computing for function Frama_C_show_each_aa
[from] Done for function Frama_C_show_each_aa
[from] Computing for function Frama_C_show_each_bb
[from] Done for function Frama_C_show_each_bb
[from] Computing for function Frama_C_show_each_cc
[from] Done for function Frama_C_show_each_cc
[from] Computing for function Frama_C_show_each_aux
[from] Done for function Frama_C_show_each_aux
[from] Computing for function sqrt
[from] Computing for function Frama_C_sqrt <-sqrt
[from] Done for function Frama_C_sqrt
[from] Done for function sqrt
[from] Computing for function Frama_C_show_each_dd
[from] Done for function Frama_C_show_each_dd
[from] Computing for function Frama_C_show_each_ee
[from] Done for function Frama_C_show_each_ee
[from] Computing for function Frama_C_show_each_ff
[from] Done for function Frama_C_show_each_ff
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function Frama_C_float_interval:
          Frama_C_entropy_source ? [--..--]
[value] Values for function sqrt:
[value] Values for function main:
          aux ? [-0. .. 8.07524668571e+21]
          tmp ? [-0. .. 89862376363.6]
          a ? [83.9759990008 .. 12666.8879961]
          b ? [-2099.83521856 .. 2094.46878047]
          c ? [-6276.20023952 .. 6306.71175755]
          d ? [-61847529062.4 .. 61847529033.6]
          e ? [-20615843020.8 .. 20615843011.2]
          f ? [-61847529062.4 .. 61847529033.6]
          Frama_C_entropy_source ? [--..--]