1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/sep.i (no preprocessing)
[value] Analyzing an incomplete application starting at f1
[value] Part of a case analysis: 0 of 0..3
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
index ∈ [--..--]
tab[0..4] ∈ [--..--]
tests/value/sep.i:36:[value] warning: function f1: precondition got status unknown.
[value] computing for function init1 <- f1.
Called from tests/value/sep.i:41.
[value] computing for function init2 <- init1 <- f1.
Called from tests/value/sep.i:18.
tests/value/sep.i:18:[kernel] warning: No code nor implicit assigns clause for function init2, generating default assigns from the prototype
[value] using specification for function init2
[value] Done for function init2
tests/value/sep.i:20:[value] warning: Statement 3: only propagating for condition false
tests/value/sep.i:26:[value] warning: Statement 6: only propagating for condition false
[value] Recording results for init1
[value] Done for function init1
[value] Recording results for f1
[value] done for function f1
[value] Next case to cover in sequential order: 1
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function init1:
res ∈ {-1}
[value:final-states] Values at end of function f1:
res ∈ {-1}
__retres ∈ {-1}
|
