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
31
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/sep.i (no preprocessing)
[value] Splitting return states on:
\return(init2) == 0, 1 (auto)
\return(init1) == 0 (auto)
[value] Analyzing an incomplete application starting at f1
[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
[value] Recording results for init1
[value] Done for function init1
[value] Recording results for f1
[value] done for function f1
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function init1:
index ∈ [--..--]
res ∈ {-1; 0}
[value:final-states] Values at end of function f1:
index ∈ [--..--]
res ∈ {-1; 0}
__retres ∈ [--..--]
|
