[kernel] Parsing tests/float/nonlin.c (with preprocessing)
tests/float/nonlin.c:75:[kernel] warning: Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30. See documentation for option -warn-decimal-float
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  Frama_C_entropy_source ∈ [--..--]
  a ∈ {0}
  b ∈ {0}
  c ∈ {0}
  r1 ∈ {0}
  r2 ∈ {0}
  d ∈ {0}
  i ∈ {0}
  s ∈ {0}
  zf ∈ {0}
  s2 ∈ {0}
  sq ∈ {0}
  h ∈ {0}
  t[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6] ∈ {7}
   [7] ∈ {8}
   [8] ∈ {9}
   [9] ∈ {10}
  r ∈ {0}
  x ∈ {0}
  y ∈ {0}
  z ∈ {0}
  rbits1 ∈ {0}
  rbits2 ∈ {0}
  v ∈ [--..--]
[value] computing for function nonlin_f <- main.
    Called from tests/float/nonlin.c:92.
[value] computing for function Frama_C_float_interval <- nonlin_f <- main.
    Called from tests/float/nonlin.c:16.
[value] using specification for function Frama_C_float_interval
share/libc/__fc_builtin.h:149:[value] function Frama_C_float_interval: precondition got status valid.
share/libc/__fc_builtin.h:150:[value] function Frama_C_float_interval: precondition got status valid.
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <- nonlin_f <- main.
    Called from tests/float/nonlin.c:17.
[value] Done for function Frama_C_float_interval
tests/float/nonlin.c:20:[value] assertion got status valid.
tests/float/nonlin.c:22:[value:nonlin] non-linear 'a + b * (c - a)', lv 'a'
tests/float/nonlin.c:22:[value:nonlin] subdividing on a
tests/float/nonlin.c:24:[value] assertion got status valid.
tests/float/nonlin.c:41:[value:nonlin] non-linear 'b * (c - a) + a', lv 'a'
tests/float/nonlin.c:41:[value:nonlin] subdividing on a
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.4000000000000p2 .. 0x1.4800000000000p2],
    {{ "r2" }},
    [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.4800000000000p2 .. 0x1.5000000000000p2],
    {{ "r2" }},
    [0x1.4800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.5000000000000p2 .. 0x1.5800000000000p2],
    {{ "r2" }},
    [0x1.5000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.5800000000000p2 .. 0x1.6000000000000p2],
    {{ "r2" }},
    [0x1.5800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.6000000000000p2 .. 0x1.6800000000000p2],
    {{ "r2" }},
    [0x1.6000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.6800000000000p2 .. 0x1.7000000000000p2],
    {{ "r2" }},
    [0x1.6800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.7000000000000p2 .. 0x1.7800000000000p2],
    {{ "r2" }},
    [0x1.7000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.7800000000000p2 .. 0x1.8000000000000p2],
    {{ "r2" }},
    [0x1.7800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.8000000000000p2 .. 0x1.8800000000000p2],
    {{ "r2" }},
    [0x1.8000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.8800000000000p2 .. 0x1.9000000000000p2],
    {{ "r2" }},
    [0x1.8800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.9000000000000p2 .. 0x1.9800000000000p2],
    {{ "r2" }},
    [0x1.9000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.9800000000000p2 .. 0x1.a000000000000p2],
    {{ "r2" }},
    [0x1.9800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.a000000000000p2 .. 0x1.a800000000000p2],
    {{ "r2" }},
    [0x1.a000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.a800000000000p2 .. 0x1.b000000000000p2],
    {{ "r2" }},
    [0x1.a800000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.b000000000000p2 .. 0x1.b800000000000p2],
    {{ "r2" }},
    [0x1.b000000000000p2 .. 0x1.c0fffffffffffp2]
tests/float/nonlin.c:42:[value] Frama_C_show_each_a_r2:
    {{ "a" }},
    [0x1.b800000000000p2 .. 0x1.c000000000000p2],
    {{ "r2" }},
    [0x1.b800000000000p2 .. 0x1.c0fffffffffffp2]
[value] Recording results for nonlin_f
[value] Done for function nonlin_f
[value] computing for function other <- main.
    Called from tests/float/nonlin.c:93.
[value] computing for function Frama_C_float_interval <- other <- main.
    Called from tests/float/nonlin.c:59.
[value] Done for function Frama_C_float_interval
[value] computing for function Frama_C_float_interval <- other <- main.
    Called from tests/float/nonlin.c:60.
[value] Done for function Frama_C_float_interval
tests/float/nonlin.c:61:[value:nonlin] non-linear 'i * i', lv 'i'
tests/float/nonlin.c:61:[value:nonlin] subdividing on i
tests/float/nonlin.c:61:[value] warning: accessing out of bounds index.
    assert (int)((double)((double)(i * i) + 2.0)) < 10;
tests/float/nonlin.c:62:[value:nonlin] non-linear 's - s', lv 's'
tests/float/nonlin.c:62:[value:nonlin] subdividing on s
tests/float/nonlin.c:63:[value:nonlin] non-linear 's - s', lv 's'
tests/float/nonlin.c:63:[value:nonlin] subdividing on s
tests/float/nonlin.c:64:[value:nonlin] non-linear 's + s', lv 's'
tests/float/nonlin.c:64:[value:nonlin] subdividing on s
tests/float/nonlin.c:65:[value:nonlin] non-linear 's * s', lv 's'
tests/float/nonlin.c:65:[value:nonlin] subdividing on s
tests/float/nonlin.c:66:[value:nonlin] non-linear 's * ((double)1 - s)', lv 's'
tests/float/nonlin.c:66:[value:nonlin] subdividing on s
[value] computing for function access_bits <- other <- main.
    Called from tests/float/nonlin.c:67.
[value] Recording results for access_bits
[value] Done for function access_bits
[value] computing for function Frama_C_interval <- other <- main.
    Called from tests/float/nonlin.c:69.
[value] using specification for function Frama_C_interval
share/libc/__fc_builtin.h:52:[value] function Frama_C_interval: precondition got status valid.
[value] Done for function Frama_C_interval
tests/float/nonlin.c:70:[value:nonlin] non-linear '(1 / x) * x', lv 'x'
tests/float/nonlin.c:70:[value:nonlin] subdividing on x
tests/float/nonlin.c:70:[value] warning: division by zero. assert x ≢ 0;
[value] Recording results for other
[value] Done for function other
[value] computing for function split_alarm <- main.
    Called from tests/float/nonlin.c:94.
tests/float/nonlin.c:74:[value] warning: non-finite float value. assert \is_finite(v);
tests/float/nonlin.c:75:[value:nonlin] non-linear '(double)ff * (double)ff', lv 'ff'
tests/float/nonlin.c:75:[value:nonlin] subdividing on ff
[value] Recording results for split_alarm
[value] Done for function split_alarm
[value] computing for function norm <- main.
    Called from tests/float/nonlin.c:95.
tests/float/nonlin.c:79:[value] warning: non-finite float value. assert \is_finite(v);
tests/float/nonlin.c:80:[value] warning: non-finite float value. assert \is_finite(v);
tests/float/nonlin.c:81:[value:nonlin] non-linear '(double)v1 * (double)v1', lv 'v1'
tests/float/nonlin.c:81:[value:nonlin] non-linear '(double)v2 * (double)v2', lv 'v2'
tests/float/nonlin.c:81:[value:nonlin] subdividing on v1
tests/float/nonlin.c:81:[value:nonlin] subdividing on v2
[value] Recording results for norm
[value] Done for function norm
[value] computing for function garbled <- main.
    Called from tests/float/nonlin.c:96.
tests/float/nonlin.c:87:[value] warning: non-finite float value.
    assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
tests/float/nonlin.c:87:[value] Assigning imprecise value to a_0.
    The imprecision originates from Arithmetic {tests/float/nonlin.c:87}
tests/float/nonlin.c:88:[value:nonlin] non-linear 'a_0 + a_0', lv 'a_0'
tests/float/nonlin.c:88:[value:nonlin] subdividing on a_0
tests/float/nonlin.c:88:[value] warning: non-finite float value. assert \is_finite(a_0);
tests/float/nonlin.c:88:[value] warning: non-finite float value. assert \is_finite((float)(a_0 + a_0));
[value] Recording results for garbled
[value] Done for function garbled
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}
  x0 ∈ [--..--]
  __retres ∈ {0; 1}
[value:final-states] Values at end of function garbled:
  a_0 ∈
     {{ garbled mix of &{x_0}
      (origin: Arithmetic {tests/float/nonlin.c:87}) }}
  f ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[value:final-states] Values at end of function nonlin_f:
  Frama_C_entropy_source ∈ [--..--]
  a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
  b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
  c ∈ {0x1.c000000000000p2}
  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
  d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[value:final-states] Values at end of function norm:
  v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
  v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
  square ∈ [-0x0.0000000000000p-1022 .. 0x1.fffffc0000020p256]
[value:final-states] Values at end of function other:
  Frama_C_entropy_source ∈ [--..--]
  i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
  s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
  zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
  s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
  sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
  h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
  r ∈ [3..11]
  x ∈ [1..42]
  y ∈ {0; 1}
  z ∈ [-171874..171874]
  rbits1 ∈ {0; 1; 2}
  rbits2 ∈ {0; 1}
[value:final-states] Values at end of function split_alarm:
  ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
  d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
[value:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
  b ∈ [-0x0.0000000000000p-1022 .. 0x1.0000000000000p0]
  c ∈ {0x1.c000000000000p2}
  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
  d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
  i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
  s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
  zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
  s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
  sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
  h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
  r ∈ [3..11]
  x ∈ [1..42]
  y ∈ {0; 1}
  z ∈ [-171874..171874]
  rbits1 ∈ {0; 1; 2}
  rbits2 ∈ {0; 1}
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function access_bits:
  rbits1 ∈ {0; 1; 2}
  x0 ∈ [--..--]
  __retres ∈ {0; 1}
[value:final-states] Values at end of function garbled:
  a_0 ∈
     {{ garbled mix of &{x_0}
      (origin: Arithmetic {tests/float/nonlin.c:87}) }}
  f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
[value:final-states] Values at end of function nonlin_f:
  Frama_C_entropy_source ∈ [--..--]
  a ∈ [5. .. 7.]
  b ∈ [-0. .. 1.]
  c ∈ {7.}
  r1 ∈ [5. .. 7.25]
  r2 ∈ [5. .. 7.015625]
  d ∈ [5. .. 7.]
[value:final-states] Values at end of function norm:
  v1 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
  v2 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
  square ∈ [-0. .. 2.31584150868e+77]
[value:final-states] Values at end of function other:
  Frama_C_entropy_source ∈ [--..--]
  i ∈ [-2.88525390625 .. 2.888671875]
  s ∈ [-133. .. 142.]
  zf ∈ [-17.1875 .. 17.1875]
  s2 ∈ [-266. .. 284.]
  sq ∈ [-0.0132904052734 .. 20164.]
  h ∈ [-20022. .. 0.598266601563]
  r ∈ [3..11]
  x ∈ [1..42]
  y ∈ {0; 1}
  z ∈ [-171874..171874]
  rbits1 ∈ {0; 1; 2}
  rbits2 ∈ {0; 1}
[value:final-states] Values at end of function split_alarm:
  ff ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
  d_0 ∈ [8.63616958461e-78 .. 1000000000.]
[value:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  a ∈ [5. .. 7.]
  b ∈ [-0. .. 1.]
  c ∈ {7.}
  r1 ∈ [5. .. 7.25]
  r2 ∈ [5. .. 7.015625]
  d ∈ [5. .. 7.]
  i ∈ [-2.88525390625 .. 2.888671875]
  s ∈ [-133. .. 142.]
  zf ∈ [-17.1875 .. 17.1875]
  s2 ∈ [-266. .. 284.]
  sq ∈ [-0.0132904052734 .. 20164.]
  h ∈ [-20022. .. 0.598266601563]
  r ∈ [3..11]
  x ∈ [1..42]
  y ∈ {0; 1}
  z ∈ [-171874..171874]
  rbits1 ∈ {0; 1; 2}
  rbits2 ∈ {0; 1}