[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/volatile.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
tests/value/volatile.c:5:[value] warning: global initialization of volatile zone G ignored
tests/value/volatile.c:11:[value] warning: global initialization of volatile zone s2.b ignored
tests/value/volatile.c:15:[value] warning: global initialization of volatile zone sv2 ignored
tests/value/volatile.c:17:[value] warning: global initialization of volatile zone sv3.b ignored
tests/value/volatile.c:18:[value] warning: global initialization of volatile zone sv4.b ignored
tests/value/volatile.c:33:[value] warning: global initialization of volatile zone nested.__anonCompField1.b ignored
tests/value/volatile.c:33:[value] warning: global initialization of volatile zone nested.__anonCompField2 ignored
tests/value/volatile.c:33:[value] warning: global initialization of volatile zone nested.t ignored
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  G ∈ [--..--]
  F ∈ [--..--]
  E ∈ [--..--]
  X ∈ [--..--]
  Y ∈ [--..--]
  pV ∈ {0}
  k ∈ {1}
  x ∈ {2}
  y ∈ {3}
  a ∈ {0}
  b ∈ {0}
  c ∈ {0}
  d ∈ {0}
  e ∈ {0}
  f ∈ {0}
  g ∈ {0}
  h ∈ {0}
  i ∈ {0}
  j ∈ {0}
  l ∈ {0}
  m ∈ {0}
  n ∈ {0}
  o ∈ {0}
  pv ∈ {0}
  s1.a ∈ {0}
    .b ∈ [--..--]
  s2.a ∈ {1}
    .b ∈ [--..--]
  sv1 ∈ [--..--]
  sv2 ∈ [--..--]
  sv3.a ∈ {3}
     .b ∈ [--..--]
  sv4.a ∈ {4}
     .b ∈ [--..--]
  nested.__anonCompField1.a ∈ {1}
        {.__anonCompField1.b; .__anonCompField2; .t[0..11]} ∈ [--..--]
        .e ∈ {0}
        .[bits 240 to 255] ∈ {0} or UNINITIALIZED
  R1 ∈ {0}
  R2 ∈ {0}
[value] computing for function main1 <- main.
        Called from tests/value/volatile.c:151.
[value] computing for function fn1 <- main1 <- main.
        Called from tests/value/volatile.c:39.
[value] Called Frama_C_show_each_1([-2147483648..2147483647])
[value] Called Frama_C_show_each_2([-2147483648..2147483647])
tests/value/volatile.c:26:[value] warning: signed overflow. assert -2147483648 ≤ x_0 + y_0;
tests/value/volatile.c:26:[value] warning: signed overflow. assert x_0 + y_0 ≤ 2147483647;
[value] Recording results for fn1
[value] Done for function fn1
[value] computing for function fn2 <- main1 <- main.
        Called from tests/value/volatile.c:40.
tests/value/volatile.c:40:[kernel] warning: Neither code nor specification for function fn2, generating default assigns from the prototype
[value] using specification for function fn2
[value] Done for function fn2
[value] Called Frama_C_show_each_d([-2147483648..2147483647])
tests/value/volatile.c:52:[value] warning: signed overflow. assert -2147483648 ≤ b - c;
tests/value/volatile.c:52:[value] warning: signed overflow. assert b - c ≤ 2147483647;
tests/value/volatile.c:53:[value] warning: signed overflow. assert -2147483648 ≤ F - F;
tests/value/volatile.c:53:[value] warning: signed overflow. assert F - F ≤ 2147483647;
tests/value/volatile.c:55:[value] warning: signed overflow. assert -2147483648 ≤ F - g;
tests/value/volatile.c:55:[value] warning: signed overflow. assert F - g ≤ 2147483647;
tests/value/volatile.c:56:[value] warning: signed overflow. assert F + 1 ≤ 2147483647;
tests/value/volatile.c:57:[value] warning: signed overflow. assert 2 + F ≤ 2147483647;
tests/value/volatile.c:58:[value] warning: signed overflow. assert -2147483648 ≤ F - l;
tests/value/volatile.c:58:[value] warning: signed overflow. assert F - l ≤ 2147483647;
tests/value/volatile.c:59:[value] warning: signed overflow. assert -2147483648 ≤ m - l;
tests/value/volatile.c:59:[value] warning: signed overflow. assert m - l ≤ 2147483647;
[value] Recording results for main1
[value] Done for function main1
[value] computing for function main2 <- main.
        Called from tests/value/volatile.c:152.
[value] Recording results for main2
[value] Done for function main2
[value] computing for function main3 <- main.
        Called from tests/value/volatile.c:153.
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert v < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(v + 1);
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert (int)(v + 1) < 1;
tests/value/volatile.c:114:[value] warning: signed overflow. assert v + 1 ≤ 2147483647;
tests/value/volatile.c:114:[value] warning: signed overflow. assert v + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert v < 2;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert a_0[v] < 1;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert v < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert v < 2;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[v] - 1);
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert (int)(a_0[v] - 1) < 1;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert v < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert v < 2;
tests/value/volatile.c:114:[value] warning: accessing out of bounds index. assert a_0[v] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ *v_ptr;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert *v_ptr < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(*v_ptr + 1);
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert (int)(*v_ptr + 1) < 1;
tests/value/volatile.c:118:[value] warning: signed overflow. assert *v_ptr + 1 ≤ 2147483647;
tests/value/volatile.c:118:[value] warning: signed overflow. assert *v_ptr + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ *v_ptr;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert *v_ptr < 2;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert a_0[*v_ptr] < 1;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ *v_ptr;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert *v_ptr < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ *v_ptr;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert *v_ptr < 2;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[*v_ptr] - 1);
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert (int)(a_0[*v_ptr] - 1) < 1;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ *v_ptr;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert *v_ptr < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert 0 ≤ *v_ptr;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert *v_ptr < 2;
tests/value/volatile.c:118:[value] warning: accessing out of bounds index. assert a_0[*v_ptr] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ svol.f[0];
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert svol.f[0] < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(svol.f[0] + 1);
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert (int)(svol.f[0] + 1) < 1;
tests/value/volatile.c:125:[value] warning: signed overflow. assert svol.f[0] + 1 ≤ 2147483647;
tests/value/volatile.c:125:[value] warning: signed overflow. assert svol.f[0] + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ svol.f[0];
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert svol.f[0] < 2;
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert a_0[svol.f[0]] < 1;
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ svol.f[0];
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert svol.f[0] < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ svol.f[0];
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert svol.f[0] < 2;
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[svol.f[0]] - 1);
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert (int)(a_0[svol.f[0]] - 1) < 1;
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ svol.f[0];
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert svol.f[0] < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert 0 ≤ svol.f[0];
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert svol.f[0] < 2;
tests/value/volatile.c:125:[value] warning: accessing out of bounds index. assert a_0[svol.f[0]] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ svol_ptr->f[0];
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert svol_ptr->f[0] < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(svol_ptr->f[0] + 1);
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert (int)(svol_ptr->f[0] + 1) < 1;
tests/value/volatile.c:129:[value] warning: signed overflow. assert svol_ptr->f[0] + 1 ≤ 2147483647;
tests/value/volatile.c:129:[value] warning: signed overflow. assert svol_ptr->f[0] + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ svol_ptr->f[0];
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert svol_ptr->f[0] < 2;
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert a_0[svol_ptr->f[0]] < 1;
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ svol_ptr->f[0];
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert svol_ptr->f[0] < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ svol_ptr->f[0];
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert svol_ptr->f[0] < 2;
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[svol_ptr->f[0]] - 1);
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert (int)(a_0[svol_ptr->f[0]] - 1) < 1;
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ svol_ptr->f[0];
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert svol_ptr->f[0] < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert 0 ≤ svol_ptr->f[0];
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert svol_ptr->f[0] < 2;
tests/value/volatile.c:129:[value] warning: accessing out of bounds index. assert a_0[svol_ptr->f[0]] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ sdeepvol.g[0];
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert sdeepvol.g[0] < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(sdeepvol.g[0] + 1);
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert (int)(sdeepvol.g[0] + 1) < 1;
tests/value/volatile.c:136:[value] warning: signed overflow. assert sdeepvol.g[0] + 1 ≤ 2147483647;
tests/value/volatile.c:136:[value] warning: signed overflow. assert sdeepvol.g[0] + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ sdeepvol.g[0];
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert sdeepvol.g[0] < 2;
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert a_0[sdeepvol.g[0]] < 1;
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ sdeepvol.g[0];
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert sdeepvol.g[0] < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ sdeepvol.g[0];
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert sdeepvol.g[0] < 2;
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[sdeepvol.g[0]] - 1);
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert (int)(a_0[sdeepvol.g[0]] - 1) < 1;
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ sdeepvol.g[0];
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert sdeepvol.g[0] < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert 0 ≤ sdeepvol.g[0];
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert sdeepvol.g[0] < 2;
tests/value/volatile.c:136:[value] warning: accessing out of bounds index. assert a_0[sdeepvol.g[0]] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ volt[0].f[0];
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert volt[0].f[0] < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(volt[0].f[0] + 1);
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert (int)(volt[0].f[0] + 1) < 1;
tests/value/volatile.c:140:[value] warning: signed overflow. assert volt[0].f[0] + 1 ≤ 2147483647;
tests/value/volatile.c:140:[value] warning: signed overflow. assert volt[0].f[0] + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ volt[0].f[0];
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert volt[0].f[0] < 2;
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert a_0[volt[0].f[0]] < 1;
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ volt[0].f[0];
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert volt[0].f[0] < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ volt[0].f[0];
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert volt[0].f[0] < 2;
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[volt[0].f[0]] - 1);
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert (int)(a_0[volt[0].f[0]] - 1) < 1;
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ volt[0].f[0];
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert volt[0].f[0] < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert 0 ≤ volt[0].f[0];
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert volt[0].f[0] < 2;
tests/value/volatile.c:140:[value] warning: accessing out of bounds index. assert a_0[volt[0].f[0]] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ deepvolt[0].g[0];
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert deepvolt[0].g[0] < 1;
[value] Called Frama_C_show_each_v([-2147483648..2147483647])
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(deepvolt[0].g[0] + 1);
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert (int)(deepvolt[0].g[0] + 1) < 1;
tests/value/volatile.c:144:[value] warning: signed overflow. assert deepvolt[0].g[0] + 1 ≤ 2147483647;
tests/value/volatile.c:144:[value] warning: signed overflow. assert deepvolt[0].g[0] + 1 ≤ 2147483647;
[value] Called Frama_C_show_each_v_plus([-2147483647..2147483647])
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ deepvolt[0].g[0];
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert deepvolt[0].g[0] < 2;
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert a_0[deepvolt[0].g[0]] < 1;
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ deepvolt[0].g[0];
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert deepvolt[0].g[0] < 2;
[value] Called Frama_C_show_each_a({0; 1})
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ deepvolt[0].g[0];
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert deepvolt[0].g[0] < 2;
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ (int)(a_0[deepvolt[0].g[0]] - 1);
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert (int)(a_0[deepvolt[0].g[0]] - 1) < 1;
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ deepvolt[0].g[0];
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert deepvolt[0].g[0] < 2;
[value] Called Frama_C_show_each_a_minus({-1; 0})
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert 0 ≤ deepvolt[0].g[0];
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert deepvolt[0].g[0] < 2;
tests/value/volatile.c:144:[value] warning: accessing out of bounds index. assert a_0[deepvolt[0].g[0]] < 1;
[value] Called Frama_C_show_each_av([-2147483648..2147483647])
[value] Recording results for main3
[value] Done for function main3
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function fn1:
  __retres ∈ [--..--]
[value:final-states] Values at end of function main1:
  G ∈ [--..--]
  E ∈ [--..--]
  X ∈ {2}
  Y ∈ [--..--]
  pV ∈ {{ &Y }}
  k ∈ [--..--]
  x ∈ {2}
  y ∈ [--..--]
  a ∈ {11; 12}
  b ∈ [--..--]
  c ∈ [--..--]
  d ∈ [--..--]
  e ∈ [--..--]
  f ∈ [--..--]
  g ∈ [--..--]
  h ∈ {1}
  l ∈ [-2147483647..2147483647]
  m ∈ [-2147483646..2147483647]
  n ∈ [--..--]
  o ∈ [--..--]
  pv ∈ {{ &X }}
  R1 ∈ [--..--]
  R2 ∈ [--..--]
[value:final-states] Values at end of function main2:
  k ∈ {{ NULL ; (int)&X }}
  p1 ∈ {{ NULL + [--..--] ; &X + [--..--] }}
  p2 ∈ {{ &X + [--..--] }}
  p3 ∈ {{ NULL + [--..--] ; &X + [--..--] }}
  __retres ∈ {{ NULL + [--..--] ; &X + [--..--] }}
[value:final-states] Values at end of function main3:
  t[0] ∈ {0}
  a_0[0] ∈ {0}
     [1] ∈ {1}
  v ∈ [--..--]
  v_ptr ∈ {{ &v }}
  svol ∈ [--..--]
  svol_ptr ∈ {{ &svol }}
  sdeepvol ∈ [--..--]
  volt[0] ∈ [--..--]
  deepvolt[0] ∈ [--..--]
[value:final-states] Values at end of function main:
  G ∈ [--..--]
  E ∈ [--..--]
  X ∈ {2}
  Y ∈ [--..--]
  pV ∈ {{ &Y }}
  k ∈ {{ NULL ; (int)&X }}
  x ∈ {2}
  y ∈ [--..--]
  a ∈ {11; 12}
  b ∈ [--..--]
  c ∈ [--..--]
  d ∈ [--..--]
  e ∈ [--..--]
  f ∈ [--..--]
  g ∈ [--..--]
  h ∈ {1}
  l ∈ [-2147483647..2147483647]
  m ∈ [-2147483646..2147483647]
  n ∈ [--..--]
  o ∈ [--..--]
  pv ∈ {{ &X }}
  R1 ∈ [--..--]
  R2 ∈ [--..--]