-
David Bühler authoredDavid Bühler authored
precise_locations.res.oracle 49.22 KiB
[kernel] Parsing tests/value/precise_locations.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
t[0..49] ∈ {0}
i ∈ {0}
j ∈ {0}
q ∈ {0}
r ∈ {0}
[eva] tests/value/precise_locations.i:29: starting to merge loop iterations
[eva] tests/value/precise_locations.i:28: starting to merge loop iterations
[eva] tests/value/precise_locations.i:33:
Frama_C_dump_each:
# Cvalue domain:
t{[0..48]{.f1[0..4]; .f_inter[0..4]; .f2#; .f_inter2[0..4]; .[bits 328 to 351]#}; [49].f1[0..4]} ∈
{0; 10} repeated %32
[49]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
i ∈ {5}
j ∈ {0; 50}
q ∈ {0}
r ∈ {0}
v ∈ [--..--]
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] tests/value/precise_locations.i:34: starting to merge loop iterations
[eva] computing for function ct <- main.
Called from tests/value/precise_locations.i:39.
[eva] Recording results for ct
[eva] Done for function ct
[eva] tests/value/precise_locations.i:38: starting to merge loop iterations
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:37: starting to merge loop iterations
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:42:
Frama_C_dump_each:
# Cvalue domain:
t[0]{.f1[0..4]; .f_inter[0..4]} ∈ {0; 10; 20}
[0].f2 ∈ [--..--]
[bits 328 to 831]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[1].f2 ∈ [--..--]
[bits 840 to 1343]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[2].f2 ∈ [--..--]
[bits 1352 to 1855]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[3].f2 ∈ [--..--]
[bits 1864 to 2367]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[4].f2 ∈ [--..--]
[bits 2376 to 2879]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[5].f2 ∈ [--..--]
[bits 2888 to 3391]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[6].f2 ∈ [--..--]
[bits 3400 to 3903]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[7].f2 ∈ [--..--]
[bits 3912 to 4415]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[8].f2 ∈ [--..--]
[bits 4424 to 4927]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[9].f2 ∈ [--..--]
[bits 4936 to 5439]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[10].f2 ∈ [--..--]
[bits 5448 to 5951]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[11].f2 ∈ [--..--]
[bits 5960 to 6463]# ∈ {0; 10; 20} repeated %32, bits 8 to 511 [12].f2 ∈ [--..--]
[bits 6472 to 6975]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[13].f2 ∈ [--..--]
[bits 6984 to 7487]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[14].f2 ∈ [--..--]
[bits 7496 to 7999]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[15].f2 ∈ [--..--]
[bits 8008 to 8511]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[16].f2 ∈ [--..--]
[bits 8520 to 9023]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[17].f2 ∈ [--..--]
[bits 9032 to 9535]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[18].f2 ∈ [--..--]
[bits 9544 to 10047]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[19].f2 ∈ [--..--]
[bits 10056 to 10559]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[20].f2 ∈ [--..--]
[bits 10568 to 11071]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[21].f2 ∈ [--..--]
[bits 11080 to 11583]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[22].f2 ∈ [--..--]
[bits 11592 to 12095]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[23].f2 ∈ [--..--]
[bits 12104 to 12607]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[24].f2 ∈ [--..--]
[bits 12616 to 13119]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[25].f2 ∈ [--..--]
[bits 13128 to 13631]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[26].f2 ∈ [--..--]
[bits 13640 to 14143]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[27].f2 ∈ [--..--]
[bits 14152 to 14655]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[28].f2 ∈ [--..--]
[bits 14664 to 15167]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[29].f2 ∈ [--..--]
[bits 15176 to 15679]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[30].f2 ∈ [--..--]
[bits 15688 to 16191]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[31].f2 ∈ [--..--]
[bits 16200 to 16703]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[32].f2 ∈ [--..--]
[bits 16712 to 17215]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[33].f2 ∈ [--..--]
[bits 17224 to 17727]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[34].f2 ∈ [--..--]
[bits 17736 to 18239]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[35].f2 ∈ [--..--]
[bits 18248 to 18751]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[36].f2 ∈ [--..--]
[bits 18760 to 19263]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[37].f2 ∈ [--..--]
[bits 19272 to 19775]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[38].f2 ∈ [--..--]
[bits 19784 to 20287]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[39].f2 ∈ [--..--]
[bits 20296 to 20799]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[40].f2 ∈ [--..--]
[bits 20808 to 21311]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[41].f2 ∈ [--..--]
[bits 21320 to 21823]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[42].f2 ∈ [--..--]
[bits 21832 to 22335]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[43].f2 ∈ [--..--]
[bits 22344 to 22847]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[44].f2 ∈ [--..--]
[bits 22856 to 23359]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[45].f2 ∈ [--..--]
[bits 23368 to 23871]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[46].f2 ∈ [--..--]
[bits 23880 to 24383]# ∈ {0; 10; 20} repeated %32, bits 8 to 511 [47].f2 ∈ [--..--]
[bits 24392 to 24895]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[48].f2 ∈ [--..--]
[bits 24904 to 25247]# ∈ {0; 10; 20} repeated %32, bits 8 to 351
[49].f_inter[0..4] ∈ {0}
[49].f2 ∈ {-99; 0}
[49]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
i ∈ {5}
j ∈ {50}
q ∈ {0}
r ∈ {0}
v ∈ [--..--]
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] using specification for function f
[eva] tests/value/precise_locations.i:48:
function f: precondition got status valid.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] using specification for function g
[eva] tests/value/precise_locations.i:49:
function g: precondition got status valid.
[eva] Done for function g
[eva] tests/value/precise_locations.i:45: starting to merge loop iterations
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] tests/value/precise_locations.i:44: starting to merge loop iterations
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva:alarm] tests/value/precise_locations.i:48: Warning:
function f: precondition got status unknown.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva:alarm] tests/value/precise_locations.i:49: Warning:
function g: precondition got status unknown.
[eva] Done for function g
[eva] Recording results for main
[eva] done for function main[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function ct:
__retres ∈ {20}
[eva:final-states] Values at end of function main:
t[0]{.f1[0..4]; .f_inter[0..4]} ∈ {0; 10; 20}
[0].f2 ∈ [--..--]
[bits 328 to 831]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[1].f2 ∈ [--..--]
[bits 840 to 1343]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[2].f2 ∈ [--..--]
[bits 1352 to 1855]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[3].f2 ∈ [--..--]
[bits 1864 to 2367]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[4].f2 ∈ [--..--]
[bits 2376 to 2879]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[5].f2 ∈ [--..--]
[bits 2888 to 3391]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[6].f2 ∈ [--..--]
[bits 3400 to 3903]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[7].f2 ∈ [--..--]
[bits 3912 to 4415]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[8].f2 ∈ [--..--]
[bits 4424 to 4927]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[9].f2 ∈ [--..--]
[bits 4936 to 5439]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[10].f2 ∈ [--..--]
[bits 5448 to 5951]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[11].f2 ∈ [--..--]
[bits 5960 to 6463]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[12].f2 ∈ [--..--]
[bits 6472 to 6975]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[13].f2 ∈ [--..--]
[bits 6984 to 7487]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[14].f2 ∈ [--..--]
[bits 7496 to 7999]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[15].f2 ∈ [--..--]
[bits 8008 to 8511]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[16].f2 ∈ [--..--]
[bits 8520 to 9023]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[17].f2 ∈ [--..--]
[bits 9032 to 9535]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[18].f2 ∈ [--..--]
[bits 9544 to 10047]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[19].f2 ∈ [--..--]
[bits 10056 to 10559]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[20].f2 ∈ [--..--]
[bits 10568 to 11071]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[21].f2 ∈ [--..--]
[bits 11080 to 11583]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[22].f2 ∈ [--..--]
[bits 11592 to 12095]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[23].f2 ∈ [--..--]
[bits 12104 to 12607]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[24].f2 ∈ [--..--]
[bits 12616 to 13119]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[25].f2 ∈ [--..--]
[bits 13128 to 13631]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[26].f2 ∈ [--..--]
[bits 13640 to 14143]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[27].f2 ∈ [--..--]
[bits 14152 to 14655]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[28].f2 ∈ [--..--]
[bits 14664 to 15167]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[29].f2 ∈ [--..--]
[bits 15176 to 15679]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[30].f2 ∈ [--..--]
[bits 15688 to 16191]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[31].f2 ∈ [--..--]
[bits 16200 to 16703]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[32].f2 ∈ [--..--] [bits 16712 to 17215]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[33].f2 ∈ [--..--]
[bits 17224 to 17727]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[34].f2 ∈ [--..--]
[bits 17736 to 18239]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[35].f2 ∈ [--..--]
[bits 18248 to 18751]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[36].f2 ∈ [--..--]
[bits 18760 to 19263]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[37].f2 ∈ [--..--]
[bits 19272 to 19775]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[38].f2 ∈ [--..--]
[bits 19784 to 20287]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[39].f2 ∈ [--..--]
[bits 20296 to 20799]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[40].f2 ∈ [--..--]
[bits 20808 to 21311]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[41].f2 ∈ [--..--]
[bits 21320 to 21823]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[42].f2 ∈ [--..--]
[bits 21832 to 22335]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[43].f2 ∈ [--..--]
[bits 22344 to 22847]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[44].f2 ∈ [--..--]
[bits 22856 to 23359]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[45].f2 ∈ [--..--]
[bits 23368 to 23871]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[46].f2 ∈ [--..--]
[bits 23880 to 24383]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[47].f2 ∈ [--..--]
[bits 24392 to 24895]# ∈ {0; 10; 20} repeated %32, bits 8 to 511
[48].f2 ∈ [--..--]
[bits 24904 to 25247]# ∈ {0; 10; 20} repeated %32, bits 8 to 351
[49].f_inter[0..4] ∈ {0}
[49].f2 ∈ {-99; 0}
[49]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
i ∈ {5}
j ∈ {50}
q ∈ [0..255]
r ∈ [0..256]
__retres ∈ [0..511]
[from] Computing for function ct
[from] Done for function ct
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
[from] Computing for function g <-main
[from] Done for function g
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function ct:
\result FROM \nothing
[from] Function f:
NO EFFECTS
[from] Function g:
NO EFFECTS
[from] Function main:
t{{[0..48]; [49].f1[0..4]}; [49].f2} FROM \nothing (and SELF)
i FROM \nothing
j FROM \nothing
q FROM t{[0..48]; [49].f1[0..4]} (and SELF)
r FROM t{[0..48]; [49].f1[0..4]} (and SELF)
\result FROM t{[0..48]; [49].f1[0..4]}; q; r
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function ct:
__retres
[inout] Inputs for function ct:
\nothing
[inout] Out (internal) for function main: t{{[0..48]; [49].f1[0..4]}; [49].f2}; i; j; q; r; __retres
[inout] Inputs for function main:
t{[0..48]; [49].f1[0..4]}; i; j; q; r
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ - ] Pre-condition (file tests/value/precise_locations.i, line 18)
tried with Call Preconditions.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
[ - ] Pre-condition (file tests/value/precise_locations.i, line 21)
tried with Call Preconditions.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
[ - ] Instance of 'Pre-condition (file tests/value/precise_locations.i, line 18)' at call 'f' (file tests/value/precise_locations.i, line 48)
tried with Eva.
[ - ] Instance of 'Pre-condition (file tests/value/precise_locations.i, line 21)' at call 'g' (file tests/value/precise_locations.i, line 49)
tried with Eva.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
2 Completely validated
2 Considered valid
4 To be validated
8 Total
--------------------------------------------------------------------------------
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
t[0..49] ∈ {0}
i ∈ {0}
j ∈ {0}
q ∈ {0}
r ∈ {0}
[eva] tests/value/precise_locations.i:33:
Frama_C_dump_each:
# Cvalue domain:
t[0].f1[0..4] ∈ {0; 10}
[0]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[1].f1[0..4] ∈ {0; 10}
[1]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[2].f1[0..4] ∈ {0; 10}
[2]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[3].f1[0..4] ∈ {0; 10}
[3]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[4].f1[0..4] ∈ {0; 10}
[4]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[5].f1[0..4] ∈ {0; 10}
[5]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0} [6].f1[0..4] ∈ {0; 10}
[6]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[7].f1[0..4] ∈ {0; 10}
[7]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[8].f1[0..4] ∈ {0; 10}
[8]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[9].f1[0..4] ∈ {0; 10}
[9]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[10].f1[0..4] ∈ {0; 10}
[10]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[11].f1[0..4] ∈ {0; 10}
[11]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[12].f1[0..4] ∈ {0; 10}
[12]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[13].f1[0..4] ∈ {0; 10}
[13]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[14].f1[0..4] ∈ {0; 10}
[14]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[15].f1[0..4] ∈ {0; 10}
[15]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[16].f1[0..4] ∈ {0; 10}
[16]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[17].f1[0..4] ∈ {0; 10}
[17]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[18].f1[0..4] ∈ {0; 10}
[18]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[19].f1[0..4] ∈ {0; 10}
[19]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[20].f1[0..4] ∈ {0; 10}
[20]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[21].f1[0..4] ∈ {0; 10}
[21]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[22].f1[0..4] ∈ {0; 10}
[22]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[23].f1[0..4] ∈ {0; 10}
[23]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[24].f1[0..4] ∈ {0; 10}
[24]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[25].f1[0..4] ∈ {0; 10}
[25]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[26].f1[0..4] ∈ {0; 10}
[26]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[27].f1[0..4] ∈ {0; 10}
[27]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[28].f1[0..4] ∈ {0; 10}
[28]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[29].f1[0..4] ∈ {0; 10}
[29]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[30].f1[0..4] ∈ {0; 10}
[30]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[31].f1[0..4] ∈ {0; 10}
[31]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[32].f1[0..4] ∈ {0; 10}
[32]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[33].f1[0..4] ∈ {0; 10}
[33]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[34].f1[0..4] ∈ {0; 10}
[34]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[35].f1[0..4] ∈ {0; 10}
[35]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[36].f1[0..4] ∈ {0; 10}
[36]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[37].f1[0..4] ∈ {0; 10}
[37]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[38].f1[0..4] ∈ {0; 10}
[38]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[39].f1[0..4] ∈ {0; 10}
[39]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[40].f1[0..4] ∈ {0; 10}
[40]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0} [41].f1[0..4] ∈ {0; 10}
[41]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[42].f1[0..4] ∈ {0; 10}
[42]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[43].f1[0..4] ∈ {0; 10}
[43]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[44].f1[0..4] ∈ {0; 10}
[44]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[45].f1[0..4] ∈ {0; 10}
[45]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[46].f1[0..4] ∈ {0; 10}
[46]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[47].f1[0..4] ∈ {0; 10}
[47]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[48].f1[0..4] ∈ {0; 10}
[48]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[49].f1[0..4] ∈ {0; 10}
[49]{.f_inter[0..4]; .f2; .f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
i ∈ {5}
j ∈ {0; 50}
q ∈ {0}
r ∈ {0}
v ∈ [--..--]
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] computing for function ct <- main.
Called from tests/value/precise_locations.i:39.
[eva] Recording results for ct
[eva] Done for function ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
[eva] tests/value/precise_locations.i:42:
Frama_C_dump_each:
# Cvalue domain:
t[0].f1[0..4] ∈ {0; 10; 20}
[0].f_inter[0..4] ∈ {0}
[0].f2 ∈ {-99; 0}
[0]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[1].f1[0..4] ∈ {0; 10; 20}
[1].f_inter[0..4] ∈ {0}
[1].f2 ∈ {-99; 0}
[1]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[2].f1[0..4] ∈ {0; 10; 20}
[2].f_inter[0..4] ∈ {0}
[2].f2 ∈ {-99; 0}
[2]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[3].f1[0..4] ∈ {0; 10; 20}
[3].f_inter[0..4] ∈ {0}
[3].f2 ∈ {-99; 0}
[3]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[4].f1[0..4] ∈ {0; 10; 20}
[4].f_inter[0..4] ∈ {0}
[4].f2 ∈ {-99; 0}
[4]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[5].f1[0..4] ∈ {0; 10; 20}
[5].f_inter[0..4] ∈ {0}
[5].f2 ∈ {-99; 0}
[5]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[6].f1[0..4] ∈ {0; 10; 20}
[6].f_inter[0..4] ∈ {0}
[6].f2 ∈ {-99; 0}
[6]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0} [7].f1[0..4] ∈ {0; 10; 20}
[7].f_inter[0..4] ∈ {0}
[7].f2 ∈ {-99; 0}
[7]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[8].f1[0..4] ∈ {0; 10; 20}
[8].f_inter[0..4] ∈ {0}
[8].f2 ∈ {-99; 0}
[8]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[9].f1[0..4] ∈ {0; 10; 20}
[9].f_inter[0..4] ∈ {0}
[9].f2 ∈ {-99; 0}
[9]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[10].f1[0..4] ∈ {0; 10; 20}
[10].f_inter[0..4] ∈ {0}
[10].f2 ∈ {-99; 0}
[10]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[11].f1[0..4] ∈ {0; 10; 20}
[11].f_inter[0..4] ∈ {0}
[11].f2 ∈ {-99; 0}
[11]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[12].f1[0..4] ∈ {0; 10; 20}
[12].f_inter[0..4] ∈ {0}
[12].f2 ∈ {-99; 0}
[12]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[13].f1[0..4] ∈ {0; 10; 20}
[13].f_inter[0..4] ∈ {0}
[13].f2 ∈ {-99; 0}
[13]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[14].f1[0..4] ∈ {0; 10; 20}
[14].f_inter[0..4] ∈ {0}
[14].f2 ∈ {-99; 0}
[14]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[15].f1[0..4] ∈ {0; 10; 20}
[15].f_inter[0..4] ∈ {0}
[15].f2 ∈ {-99; 0}
[15]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[16].f1[0..4] ∈ {0; 10; 20}
[16].f_inter[0..4] ∈ {0}
[16].f2 ∈ {-99; 0}
[16]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[17].f1[0..4] ∈ {0; 10; 20}
[17].f_inter[0..4] ∈ {0}
[17].f2 ∈ {-99; 0}
[17]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[18].f1[0..4] ∈ {0; 10; 20}
[18].f_inter[0..4] ∈ {0}
[18].f2 ∈ {-99; 0}
[18]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[19].f1[0..4] ∈ {0; 10; 20}
[19].f_inter[0..4] ∈ {0}
[19].f2 ∈ {-99; 0}
[19]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[20].f1[0..4] ∈ {0; 10; 20}
[20].f_inter[0..4] ∈ {0}
[20].f2 ∈ {-99; 0}
[20]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[21].f1[0..4] ∈ {0; 10; 20}
[21].f_inter[0..4] ∈ {0}
[21].f2 ∈ {-99; 0}
[21]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[22].f1[0..4] ∈ {0; 10; 20}
[22].f_inter[0..4] ∈ {0}
[22].f2 ∈ {-99; 0}
[22]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[23].f1[0..4] ∈ {0; 10; 20}
[23].f_inter[0..4] ∈ {0}
[23].f2 ∈ {-99; 0}
[23]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[24].f1[0..4] ∈ {0; 10; 20}
[24].f_inter[0..4] ∈ {0} [24].f2 ∈ {-99; 0}
[24]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[25].f1[0..4] ∈ {0; 10; 20}
[25].f_inter[0..4] ∈ {0}
[25].f2 ∈ {-99; 0}
[25]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[26].f1[0..4] ∈ {0; 10; 20}
[26].f_inter[0..4] ∈ {0}
[26].f2 ∈ {-99; 0}
[26]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[27].f1[0..4] ∈ {0; 10; 20}
[27].f_inter[0..4] ∈ {0}
[27].f2 ∈ {-99; 0}
[27]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[28].f1[0..4] ∈ {0; 10; 20}
[28].f_inter[0..4] ∈ {0}
[28].f2 ∈ {-99; 0}
[28]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[29].f1[0..4] ∈ {0; 10; 20}
[29].f_inter[0..4] ∈ {0}
[29].f2 ∈ {-99; 0}
[29]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[30].f1[0..4] ∈ {0; 10; 20}
[30].f_inter[0..4] ∈ {0}
[30].f2 ∈ {-99; 0}
[30]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[31].f1[0..4] ∈ {0; 10; 20}
[31].f_inter[0..4] ∈ {0}
[31].f2 ∈ {-99; 0}
[31]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[32].f1[0..4] ∈ {0; 10; 20}
[32].f_inter[0..4] ∈ {0}
[32].f2 ∈ {-99; 0}
[32]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[33].f1[0..4] ∈ {0; 10; 20}
[33].f_inter[0..4] ∈ {0}
[33].f2 ∈ {-99; 0}
[33]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[34].f1[0..4] ∈ {0; 10; 20}
[34].f_inter[0..4] ∈ {0}
[34].f2 ∈ {-99; 0}
[34]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[35].f1[0..4] ∈ {0; 10; 20}
[35].f_inter[0..4] ∈ {0}
[35].f2 ∈ {-99; 0}
[35]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[36].f1[0..4] ∈ {0; 10; 20}
[36].f_inter[0..4] ∈ {0}
[36].f2 ∈ {-99; 0}
[36]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[37].f1[0..4] ∈ {0; 10; 20}
[37].f_inter[0..4] ∈ {0}
[37].f2 ∈ {-99; 0}
[37]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[38].f1[0..4] ∈ {0; 10; 20}
[38].f_inter[0..4] ∈ {0}
[38].f2 ∈ {-99; 0}
[38]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[39].f1[0..4] ∈ {0; 10; 20}
[39].f_inter[0..4] ∈ {0}
[39].f2 ∈ {-99; 0}
[39]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[40].f1[0..4] ∈ {0; 10; 20}
[40].f_inter[0..4] ∈ {0}
[40].f2 ∈ {-99; 0}
[40]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[41].f1[0..4] ∈ {0; 10; 20}
[41].f_inter[0..4] ∈ {0}
[41].f2 ∈ {-99; 0}
[41]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0} [42].f1[0..4] ∈ {0; 10; 20}
[42].f_inter[0..4] ∈ {0}
[42].f2 ∈ {-99; 0}
[42]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[43].f1[0..4] ∈ {0; 10; 20}
[43].f_inter[0..4] ∈ {0}
[43].f2 ∈ {-99; 0}
[43]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[44].f1[0..4] ∈ {0; 10; 20}
[44].f_inter[0..4] ∈ {0}
[44].f2 ∈ {-99; 0}
[44]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[45].f1[0..4] ∈ {0; 10; 20}
[45].f_inter[0..4] ∈ {0}
[45].f2 ∈ {-99; 0}
[45]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[46].f1[0..4] ∈ {0; 10; 20}
[46].f_inter[0..4] ∈ {0}
[46].f2 ∈ {-99; 0}
[46]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[47].f1[0..4] ∈ {0; 10; 20}
[47].f_inter[0..4] ∈ {0}
[47].f2 ∈ {-99; 0}
[47]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[48].f1[0..4] ∈ {0; 10; 20}
[48].f_inter[0..4] ∈ {0}
[48].f2 ∈ {-99; 0}
[48]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[49].f1[0..4] ∈ {0; 10; 20}
[49].f_inter[0..4] ∈ {0}
[49].f2 ∈ {-99; 0}
[49]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
i ∈ {5}
j ∈ {50}
q ∈ {0}
r ∈ {0}
v ∈ [--..--]
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main. Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] computing for function f <- main.
Called from tests/value/precise_locations.i:48.
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/value/precise_locations.i:49.
[eva] Done for function g
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function ct:
__retres ∈ {20}
[eva:final-states] Values at end of function main:
t[0].f1[0..4] ∈ {0; 10; 20}
[0].f_inter[0..4] ∈ {0}
[0].f2 ∈ {-99; 0}
[0]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[1].f1[0..4] ∈ {0; 10; 20}
[1].f_inter[0..4] ∈ {0}
[1].f2 ∈ {-99; 0}
[1]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[2].f1[0..4] ∈ {0; 10; 20}
[2].f_inter[0..4] ∈ {0}
[2].f2 ∈ {-99; 0}
[2]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[3].f1[0..4] ∈ {0; 10; 20}
[3].f_inter[0..4] ∈ {0}
[3].f2 ∈ {-99; 0}
[3]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[4].f1[0..4] ∈ {0; 10; 20}
[4].f_inter[0..4] ∈ {0}
[4].f2 ∈ {-99; 0}
[4]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[5].f1[0..4] ∈ {0; 10; 20}
[5].f_inter[0..4] ∈ {0}
[5].f2 ∈ {-99; 0}
[5]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[6].f1[0..4] ∈ {0; 10; 20}
[6].f_inter[0..4] ∈ {0}
[6].f2 ∈ {-99; 0}
[6]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[7].f1[0..4] ∈ {0; 10; 20}
[7].f_inter[0..4] ∈ {0}
[7].f2 ∈ {-99; 0}
[7]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[8].f1[0..4] ∈ {0; 10; 20}
[8].f_inter[0..4] ∈ {0}
[8].f2 ∈ {-99; 0}
[8]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[9].f1[0..4] ∈ {0; 10; 20}
[9].f_inter[0..4] ∈ {0}
[9].f2 ∈ {-99; 0}
[9]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[10].f1[0..4] ∈ {0; 10; 20}
[10].f_inter[0..4] ∈ {0}
[10].f2 ∈ {-99; 0}
[10]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[11].f1[0..4] ∈ {0; 10; 20}
[11].f_inter[0..4] ∈ {0}
[11].f2 ∈ {-99; 0}
[11]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[12].f1[0..4] ∈ {0; 10; 20}
[12].f_inter[0..4] ∈ {0}
[12].f2 ∈ {-99; 0}
[12]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[13].f1[0..4] ∈ {0; 10; 20} [13].f_inter[0..4] ∈ {0}
[13].f2 ∈ {-99; 0}
[13]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[14].f1[0..4] ∈ {0; 10; 20}
[14].f_inter[0..4] ∈ {0}
[14].f2 ∈ {-99; 0}
[14]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[15].f1[0..4] ∈ {0; 10; 20}
[15].f_inter[0..4] ∈ {0}
[15].f2 ∈ {-99; 0}
[15]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[16].f1[0..4] ∈ {0; 10; 20}
[16].f_inter[0..4] ∈ {0}
[16].f2 ∈ {-99; 0}
[16]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[17].f1[0..4] ∈ {0; 10; 20}
[17].f_inter[0..4] ∈ {0}
[17].f2 ∈ {-99; 0}
[17]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[18].f1[0..4] ∈ {0; 10; 20}
[18].f_inter[0..4] ∈ {0}
[18].f2 ∈ {-99; 0}
[18]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[19].f1[0..4] ∈ {0; 10; 20}
[19].f_inter[0..4] ∈ {0}
[19].f2 ∈ {-99; 0}
[19]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[20].f1[0..4] ∈ {0; 10; 20}
[20].f_inter[0..4] ∈ {0}
[20].f2 ∈ {-99; 0}
[20]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[21].f1[0..4] ∈ {0; 10; 20}
[21].f_inter[0..4] ∈ {0}
[21].f2 ∈ {-99; 0}
[21]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[22].f1[0..4] ∈ {0; 10; 20}
[22].f_inter[0..4] ∈ {0}
[22].f2 ∈ {-99; 0}
[22]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[23].f1[0..4] ∈ {0; 10; 20}
[23].f_inter[0..4] ∈ {0}
[23].f2 ∈ {-99; 0}
[23]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[24].f1[0..4] ∈ {0; 10; 20}
[24].f_inter[0..4] ∈ {0}
[24].f2 ∈ {-99; 0}
[24]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[25].f1[0..4] ∈ {0; 10; 20}
[25].f_inter[0..4] ∈ {0}
[25].f2 ∈ {-99; 0}
[25]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[26].f1[0..4] ∈ {0; 10; 20}
[26].f_inter[0..4] ∈ {0}
[26].f2 ∈ {-99; 0}
[26]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[27].f1[0..4] ∈ {0; 10; 20}
[27].f_inter[0..4] ∈ {0}
[27].f2 ∈ {-99; 0}
[27]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[28].f1[0..4] ∈ {0; 10; 20}
[28].f_inter[0..4] ∈ {0}
[28].f2 ∈ {-99; 0}
[28]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[29].f1[0..4] ∈ {0; 10; 20}
[29].f_inter[0..4] ∈ {0}
[29].f2 ∈ {-99; 0}
[29]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[30].f1[0..4] ∈ {0; 10; 20}
[30].f_inter[0..4] ∈ {0}
[30].f2 ∈ {-99; 0} [30]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[31].f1[0..4] ∈ {0; 10; 20}
[31].f_inter[0..4] ∈ {0}
[31].f2 ∈ {-99; 0}
[31]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[32].f1[0..4] ∈ {0; 10; 20}
[32].f_inter[0..4] ∈ {0}
[32].f2 ∈ {-99; 0}
[32]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[33].f1[0..4] ∈ {0; 10; 20}
[33].f_inter[0..4] ∈ {0}
[33].f2 ∈ {-99; 0}
[33]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[34].f1[0..4] ∈ {0; 10; 20}
[34].f_inter[0..4] ∈ {0}
[34].f2 ∈ {-99; 0}
[34]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[35].f1[0..4] ∈ {0; 10; 20}
[35].f_inter[0..4] ∈ {0}
[35].f2 ∈ {-99; 0}
[35]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[36].f1[0..4] ∈ {0; 10; 20}
[36].f_inter[0..4] ∈ {0}
[36].f2 ∈ {-99; 0}
[36]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[37].f1[0..4] ∈ {0; 10; 20}
[37].f_inter[0..4] ∈ {0}
[37].f2 ∈ {-99; 0}
[37]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[38].f1[0..4] ∈ {0; 10; 20}
[38].f_inter[0..4] ∈ {0}
[38].f2 ∈ {-99; 0}
[38]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[39].f1[0..4] ∈ {0; 10; 20}
[39].f_inter[0..4] ∈ {0}
[39].f2 ∈ {-99; 0}
[39]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[40].f1[0..4] ∈ {0; 10; 20}
[40].f_inter[0..4] ∈ {0}
[40].f2 ∈ {-99; 0}
[40]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[41].f1[0..4] ∈ {0; 10; 20}
[41].f_inter[0..4] ∈ {0}
[41].f2 ∈ {-99; 0}
[41]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[42].f1[0..4] ∈ {0; 10; 20}
[42].f_inter[0..4] ∈ {0}
[42].f2 ∈ {-99; 0}
[42]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[43].f1[0..4] ∈ {0; 10; 20}
[43].f_inter[0..4] ∈ {0}
[43].f2 ∈ {-99; 0}
[43]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[44].f1[0..4] ∈ {0; 10; 20}
[44].f_inter[0..4] ∈ {0}
[44].f2 ∈ {-99; 0}
[44]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[45].f1[0..4] ∈ {0; 10; 20}
[45].f_inter[0..4] ∈ {0}
[45].f2 ∈ {-99; 0}
[45]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[46].f1[0..4] ∈ {0; 10; 20}
[46].f_inter[0..4] ∈ {0}
[46].f2 ∈ {-99; 0}
[46]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[47].f1[0..4] ∈ {0; 10; 20}
[47].f_inter[0..4] ∈ {0}
[47].f2 ∈ {-99; 0}
[47]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[48].f1[0..4] ∈ {0; 10; 20} [48].f_inter[0..4] ∈ {0}
[48].f2 ∈ {-99; 0}
[48]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
[49].f1[0..4] ∈ {0; 10; 20}
[49].f_inter[0..4] ∈ {0}
[49].f2 ∈ {-99; 0}
[49]{.f_inter2[0..4]; .[bits 328 to 351]} ∈ {0}
i ∈ {5}
j ∈ {50}
q ∈ {0; 10; 20}
r ∈ {0; 1; 11; 21}
__retres ∈ {0; 1; 10; 11; 20; 21; 31; 41}
[from] Computing for function ct
[from] Done for function ct
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
[from] Computing for function g <-main
[from] Done for function g
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function ct:
\result FROM \nothing
[from] Function f:
NO EFFECTS
[from] Function g:
NO EFFECTS
[from] Function main:
t{[0].f1[0..4]; [0].f2; [1].f1[0..4]; [1].f2; [2].f1[0..4]; [2].f2;
[3].f1[0..4]; [3].f2; [4].f1[0..4]; [4].f2; [5].f1[0..4]; [5].f2;
[6].f1[0..4]; [6].f2; [7].f1[0..4]; [7].f2; [8].f1[0..4]; [8].f2;
[9].f1[0..4]; [9].f2; [10].f1[0..4]; [10].f2; [11].f1[0..4]; [11].f2;
[12].f1[0..4]; [12].f2; [13].f1[0..4]; [13].f2; [14].f1[0..4]; [14].f2;
[15].f1[0..4]; [15].f2; [16].f1[0..4]; [16].f2; [17].f1[0..4]; [17].f2;
[18].f1[0..4]; [18].f2; [19].f1[0..4]; [19].f2; [20].f1[0..4]; [20].f2;
[21].f1[0..4]; [21].f2; [22].f1[0..4]; [22].f2; [23].f1[0..4]; [23].f2;
[24].f1[0..4]; [24].f2; [25].f1[0..4]; [25].f2; [26].f1[0..4]; [26].f2;
[27].f1[0..4]; [27].f2; [28].f1[0..4]; [28].f2; [29].f1[0..4]; [29].f2;
[30].f1[0..4]; [30].f2; [31].f1[0..4]; [31].f2; [32].f1[0..4]; [32].f2;
[33].f1[0..4]; [33].f2; [34].f1[0..4]; [34].f2; [35].f1[0..4]; [35].f2;
[36].f1[0..4]; [36].f2; [37].f1[0..4]; [37].f2; [38].f1[0..4]; [38].f2;
[39].f1[0..4]; [39].f2; [40].f1[0..4]; [40].f2; [41].f1[0..4]; [41].f2;
[42].f1[0..4]; [42].f2; [43].f1[0..4]; [43].f2; [44].f1[0..4]; [44].f2;
[45].f1[0..4]; [45].f2; [46].f1[0..4]; [46].f2; [47].f1[0..4]; [47].f2;
[48].f1[0..4]; [48].f2; [49].f1[0..4]; [49].f2}
FROM \nothing (and SELF)
i FROM \nothing
j FROM \nothing
q FROM t{[0].f1[0..4]; [1].f1[0..4]; [2].f1[0..4]; [3].f1[0..4];
[4].f1[0..4]; [5].f1[0..4]; [6].f1[0..4]; [7].f1[0..4];
[8].f1[0..4]; [9].f1[0..4]; [10].f1[0..4]; [11].f1[0..4];
[12].f1[0..4]; [13].f1[0..4]; [14].f1[0..4]; [15].f1[0..4];
[16].f1[0..4]; [17].f1[0..4]; [18].f1[0..4]; [19].f1[0..4];
[20].f1[0..4]; [21].f1[0..4]; [22].f1[0..4]; [23].f1[0..4];
[24].f1[0..4]; [25].f1[0..4]; [26].f1[0..4]; [27].f1[0..4];
[28].f1[0..4]; [29].f1[0..4]; [30].f1[0..4]; [31].f1[0..4];
[32].f1[0..4]; [33].f1[0..4]; [34].f1[0..4]; [35].f1[0..4];
[36].f1[0..4]; [37].f1[0..4]; [38].f1[0..4]; [39].f1[0..4];
[40].f1[0..4]; [41].f1[0..4]; [42].f1[0..4]; [43].f1[0..4];
[44].f1[0..4]; [45].f1[0..4]; [46].f1[0..4]; [47].f1[0..4];
[48].f1[0..4]; [49].f1[0..4]} (and SELF)
r FROM t{[0].f1[0..4]; [1].f1[0..4]; [2].f1[0..4]; [3].f1[0..4];
[4].f1[0..4]; [5].f1[0..4]; [6].f1[0..4]; [7].f1[0..4];
[8].f1[0..4]; [9].f1[0..4]; [10].f1[0..4]; [11].f1[0..4];
[12].f1[0..4]; [13].f1[0..4]; [14].f1[0..4]; [15].f1[0..4];
[16].f1[0..4]; [17].f1[0..4]; [18].f1[0..4]; [19].f1[0..4];
[20].f1[0..4]; [21].f1[0..4]; [22].f1[0..4]; [23].f1[0..4];
[24].f1[0..4]; [25].f1[0..4]; [26].f1[0..4]; [27].f1[0..4];
[28].f1[0..4]; [29].f1[0..4]; [30].f1[0..4]; [31].f1[0..4]; [32].f1[0..4]; [33].f1[0..4]; [34].f1[0..4]; [35].f1[0..4];
[36].f1[0..4]; [37].f1[0..4]; [38].f1[0..4]; [39].f1[0..4];
[40].f1[0..4]; [41].f1[0..4]; [42].f1[0..4]; [43].f1[0..4];
[44].f1[0..4]; [45].f1[0..4]; [46].f1[0..4]; [47].f1[0..4];
[48].f1[0..4]; [49].f1[0..4]} (and SELF)
\result FROM t{[0].f1[0..4]; [1].f1[0..4]; [2].f1[0..4]; [3].f1[0..4];
[4].f1[0..4]; [5].f1[0..4]; [6].f1[0..4]; [7].f1[0..4];
[8].f1[0..4]; [9].f1[0..4]; [10].f1[0..4]; [11].f1[0..4];
[12].f1[0..4]; [13].f1[0..4]; [14].f1[0..4]; [15].f1[0..4];
[16].f1[0..4]; [17].f1[0..4]; [18].f1[0..4]; [19].f1[0..4];
[20].f1[0..4]; [21].f1[0..4]; [22].f1[0..4]; [23].f1[0..4];
[24].f1[0..4]; [25].f1[0..4]; [26].f1[0..4]; [27].f1[0..4];
[28].f1[0..4]; [29].f1[0..4]; [30].f1[0..4]; [31].f1[0..4];
[32].f1[0..4]; [33].f1[0..4]; [34].f1[0..4]; [35].f1[0..4];
[36].f1[0..4]; [37].f1[0..4]; [38].f1[0..4]; [39].f1[0..4];
[40].f1[0..4]; [41].f1[0..4]; [42].f1[0..4]; [43].f1[0..4];
[44].f1[0..4]; [45].f1[0..4]; [46].f1[0..4]; [47].f1[0..4];
[48].f1[0..4]; [49].f1[0..4]};
q; r
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function ct:
__retres
[inout] Inputs for function ct:
\nothing
[inout] InOut (internal) for function ct:
Operational inputs:
\nothing
Operational inputs on termination:
\nothing
Sure outputs:
__retres
[inout] Out (internal) for function main:
t{[0].f1[0..4]; [0].f2; [1].f1[0..4]; [1].f2; [2].f1[0..4]; [2].f2;
[3].f1[0..4]; [3].f2; [4].f1[0..4]; [4].f2; [5].f1[0..4]; [5].f2;
[6].f1[0..4]; [6].f2; [7].f1[0..4]; [7].f2; [8].f1[0..4]; [8].f2;
[9].f1[0..4]; [9].f2; [10].f1[0..4]; [10].f2; [11].f1[0..4]; [11].f2;
[12].f1[0..4]; [12].f2; [13].f1[0..4]; [13].f2; [14].f1[0..4]; [14].f2;
[15].f1[0..4]; [15].f2; [16].f1[0..4]; [16].f2; [17].f1[0..4]; [17].f2;
[18].f1[0..4]; [18].f2; [19].f1[0..4]; [19].f2; [20].f1[0..4]; [20].f2;
[21].f1[0..4]; [21].f2; [22].f1[0..4]; [22].f2; [23].f1[0..4]; [23].f2;
[24].f1[0..4]; [24].f2; [25].f1[0..4]; [25].f2; [26].f1[0..4]; [26].f2;
[27].f1[0..4]; [27].f2; [28].f1[0..4]; [28].f2; [29].f1[0..4]; [29].f2;
[30].f1[0..4]; [30].f2; [31].f1[0..4]; [31].f2; [32].f1[0..4]; [32].f2;
[33].f1[0..4]; [33].f2; [34].f1[0..4]; [34].f2; [35].f1[0..4]; [35].f2;
[36].f1[0..4]; [36].f2; [37].f1[0..4]; [37].f2; [38].f1[0..4]; [38].f2;
[39].f1[0..4]; [39].f2; [40].f1[0..4]; [40].f2; [41].f1[0..4]; [41].f2;
[42].f1[0..4]; [42].f2; [43].f1[0..4]; [43].f2; [44].f1[0..4]; [44].f2;
[45].f1[0..4]; [45].f2; [46].f1[0..4]; [46].f2; [47].f1[0..4]; [47].f2;
[48].f1[0..4]; [48].f2; [49].f1[0..4]; [49].f2}; i; j; q; r; __retres
[inout] Inputs for function main:
t{[0].f1[0..4]; [1].f1[0..4]; [2].f1[0..4]; [3].f1[0..4]; [4].f1[0..4];
[5].f1[0..4]; [6].f1[0..4]; [7].f1[0..4]; [8].f1[0..4]; [9].f1[0..4];
[10].f1[0..4]; [11].f1[0..4]; [12].f1[0..4]; [13].f1[0..4];
[14].f1[0..4]; [15].f1[0..4]; [16].f1[0..4]; [17].f1[0..4];
[18].f1[0..4]; [19].f1[0..4]; [20].f1[0..4]; [21].f1[0..4];
[22].f1[0..4]; [23].f1[0..4]; [24].f1[0..4]; [25].f1[0..4];
[26].f1[0..4]; [27].f1[0..4]; [28].f1[0..4]; [29].f1[0..4];
[30].f1[0..4]; [31].f1[0..4]; [32].f1[0..4]; [33].f1[0..4];
[34].f1[0..4]; [35].f1[0..4]; [36].f1[0..4]; [37].f1[0..4];
[38].f1[0..4]; [39].f1[0..4]; [40].f1[0..4]; [41].f1[0..4];
[42].f1[0..4]; [43].f1[0..4]; [44].f1[0..4]; [45].f1[0..4];
[46].f1[0..4]; [47].f1[0..4]; [48].f1[0..4]; [49].f1[0..4]}; i; j;
q; r
[inout] InOut (internal) for function main:
Operational inputs:
t{[0].f1[0..4]; [1].f1[0..4]; [2].f1[0..4]; [3].f1[0..4]; [4].f1[0..4];
[5].f1[0..4]; [6].f1[0..4]; [7].f1[0..4]; [8].f1[0..4]; [9].f1[0..4];
[10].f1[0..4]; [11].f1[0..4]; [12].f1[0..4]; [13].f1[0..4];
[14].f1[0..4]; [15].f1[0..4]; [16].f1[0..4]; [17].f1[0..4];
[18].f1[0..4]; [19].f1[0..4]; [20].f1[0..4]; [21].f1[0..4]; [22].f1[0..4]; [23].f1[0..4]; [24].f1[0..4]; [25].f1[0..4];
[26].f1[0..4]; [27].f1[0..4]; [28].f1[0..4]; [29].f1[0..4];
[30].f1[0..4]; [31].f1[0..4]; [32].f1[0..4]; [33].f1[0..4];
[34].f1[0..4]; [35].f1[0..4]; [36].f1[0..4]; [37].f1[0..4];
[38].f1[0..4]; [39].f1[0..4]; [40].f1[0..4]; [41].f1[0..4];
[42].f1[0..4]; [43].f1[0..4]; [44].f1[0..4]; [45].f1[0..4];
[46].f1[0..4]; [47].f1[0..4]; [48].f1[0..4]; [49].f1[0..4]}; q; r
Operational inputs on termination:
t{[0].f1[0..4]; [1].f1[0..4]; [2].f1[0..4]; [3].f1[0..4]; [4].f1[0..4];
[5].f1[0..4]; [6].f1[0..4]; [7].f1[0..4]; [8].f1[0..4]; [9].f1[0..4];
[10].f1[0..4]; [11].f1[0..4]; [12].f1[0..4]; [13].f1[0..4];
[14].f1[0..4]; [15].f1[0..4]; [16].f1[0..4]; [17].f1[0..4];
[18].f1[0..4]; [19].f1[0..4]; [20].f1[0..4]; [21].f1[0..4];
[22].f1[0..4]; [23].f1[0..4]; [24].f1[0..4]; [25].f1[0..4];
[26].f1[0..4]; [27].f1[0..4]; [28].f1[0..4]; [29].f1[0..4];
[30].f1[0..4]; [31].f1[0..4]; [32].f1[0..4]; [33].f1[0..4];
[34].f1[0..4]; [35].f1[0..4]; [36].f1[0..4]; [37].f1[0..4];
[38].f1[0..4]; [39].f1[0..4]; [40].f1[0..4]; [41].f1[0..4];
[42].f1[0..4]; [43].f1[0..4]; [44].f1[0..4]; [45].f1[0..4];
[46].f1[0..4]; [47].f1[0..4]; [48].f1[0..4]; [49].f1[0..4]}; q; r
Sure outputs:
i; j; __retres
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ Valid ] Pre-condition (file tests/value/precise_locations.i, line 18)
by Call Preconditions.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
[ Valid ] Pre-condition (file tests/value/precise_locations.i, line 21)
by Call Preconditions.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
[ Valid ] Instance of 'Pre-condition (file tests/value/precise_locations.i, line 18)' at call 'f' (file tests/value/precise_locations.i, line 48)
by Eva (v2).
[ Valid ] Instance of 'Pre-condition (file tests/value/precise_locations.i, line 21)' at call 'g' (file tests/value/precise_locations.i, line 49)
by Eva (v2).
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
6 Completely validated
2 Considered valid
8 Total
--------------------------------------------------------------------------------