[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/array_access.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  t1[0] ∈ {1}
    [1] ∈ {2}
    [2] ∈ {3}
    [3] ∈ {4}
    [4] ∈ {5}
    [5] ∈ {6}
    [6] ∈ {7}
    [7] ∈ {8}
    [8] ∈ {9}
  t2[0] ∈ {11}
    [1] ∈ {12}
    [2] ∈ {13}
    [3] ∈ {14}
    [4] ∈ {15}
    [5] ∈ {16}
    [6] ∈ {17}
    [7] ∈ {18}
    [8] ∈ {19}
  ch[0] ∈ {0}
    [1] ∈ {1}
    [2] ∈ {0}
    [3] ∈ {1}
    [4] ∈ {0}
    [5] ∈ {1}
    [6] ∈ {0}
    [7] ∈ {1}
    [8] ∈ {0}
    [9] ∈ {1}
    [10] ∈ {0}
    [11] ∈ {1}
    [12] ∈ {0}
    [13] ∈ {1}
    [14] ∈ {0}
    [15..17] ∈ {1}
    [18] ∈ {0}
    [19] ∈ {1}
    [20] ∈ {0}
    [21] ∈ {1}
    [22] ∈ {0}
    [23] ∈ {1}
    [24] ∈ {0}
    [25] ∈ {1}
    [26] ∈ {0}
    [27] ∈ {1}
    [28] ∈ {0}
    [29] ∈ {1}
    [30] ∈ {0}
    [31] ∈ {1}
    [32] ∈ {0}
    [33] ∈ {1}
    [34] ∈ {0}
    [35] ∈ {1}
    [36] ∈ {0}
    [37] ∈ {1}
    [38] ∈ {0}
    [39] ∈ {1}
    [40] ∈ {0}
    [41] ∈ {1}
    [42] ∈ {0}
    [43] ∈ {1}
    [44] ∈ {0}
    [45] ∈ {1}
    [46] ∈ {0}
    [47] ∈ {1}
    [48] ∈ {0}
    [49] ∈ {1}
    [50] ∈ {0}
    [51] ∈ {1}
    [52] ∈ {0}
    [53] ∈ {1}
    [54] ∈ {0}
    [55] ∈ {1}
    [56] ∈ {0}
    [57] ∈ {1}
    [58] ∈ {0}
    [59] ∈ {1}
    [60] ∈ {0}
    [61] ∈ {1}
    [62] ∈ {0}
    [63] ∈ {1}
    [64] ∈ {0}
    [65] ∈ {1}
    [66] ∈ {0}
    [67] ∈ {1}
    [68] ∈ {0}
    [69] ∈ {1}
    [70] ∈ {0}
    [71] ∈ {1}
    [72] ∈ {0}
    [73] ∈ {1}
    [74] ∈ {0}
    [75] ∈ {1}
    [76] ∈ {0}
    [77] ∈ {1}
    [78] ∈ {0}
    [79] ∈ {1}
    [80] ∈ {0}
    [81] ∈ {1}
    [82] ∈ {0}
    [83] ∈ {1}
    [84] ∈ {0}
    [85] ∈ {1}
    [86] ∈ {0}
    [87] ∈ {1}
    [88] ∈ {0}
    [89] ∈ {1}
    [90] ∈ {0}
    [91] ∈ {1}
    [92] ∈ {0}
    [93] ∈ {1}
    [94] ∈ {0}
    [95] ∈ {1}
    [96] ∈ {0}
    [97] ∈ {1}
    [98] ∈ {0}
    [99] ∈ {1}
    [100] ∈ {0}
    [101] ∈ {1}
    [102] ∈ {0}
    [103] ∈ {1}
    [104] ∈ {2}
    [105] ∈ {3}
    [106] ∈ {4}
  R ∈ {0}
[value] Call to builtin bzero(({{ (unsigned char *)&LT }},{40}))
[value] computing for function any_int <- main.
        Called from tests/value/array_access.c:16.
[value] using specification for function any_int
[value] Done for function any_int
[value] computing for function any_int <- main.
        Called from tests/value/array_access.c:16.
[value] Done for function any_int
[value] Called Frama_C_show_each_I([0..8])
tests/value/array_access.c:19:[value] warning: accessing out of bounds index. assert 0 ≤ (int)((int)(-i) - 1);
tests/value/array_access.c:19:[value] warning: accessing out of bounds index. assert (int)((int)(-i) - 1) < 10;
[value] computing for function any_int <- main.
        Called from tests/value/array_access.c:21.
[value] Done for function any_int
tests/value/array_access.c:21:[value] warning: out of bounds read.
                 assert \valid_read((int *)((char *)ch) + tmp_0);
                 (tmp_0 from any_int())
[value] Recording results for main
[value] done for function main
tests/value/array_access.c:19:[value] assertion 'Value,index_bound' got final status valid.
tests/value/array_access.c:19:[value] assertion 'Value,index_bound' got final status invalid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
  R ∈ {16777472; 16777473}
  i ∈ [--..--]
  j ∈ {10}
  k ∈ {88}
  c ∈ [--..--]
  p ∈ UNINITIALIZED
  LT[0] ∈ {1}
    [1..9] ∈ {0}
[from] Computing for function main
[from] Computing for function Frama_C_bzero <-main
[from] Done for function Frama_C_bzero
[from] Computing for function any_int <-main
[from] Done for function any_int
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_bzero:
  LT[0..9] FROM \nothing
[from] Function any_int:
  \result FROM \nothing
[from] Function main:
  R FROM ch[0..103]
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
          R; i; j; k; c; p; LT[0..9]; tmp; tmp_0
[inout] Inputs for function main:
          t1[0..8]; t2[0..8]; ch[0..103]