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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/origin.i (no preprocessing)
[value] Analyzing a complete application starting at origin
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
a ∈ {0}
b ∈ {0}
aa2 ∈ {0}
p ∈ {0}
pa1 ∈ {0}
pa2 ∈ {0}
qa2 ∈ {0}
pa3 ∈ {0}
q ∈ {0}
t[0..11] ∈ {0}
tt[0..9] ∈ {0}
ta1[0..9] ∈ {0}
ta2[0..9] ∈ {0}
ta3[0..9] ∈ {0}
tta2[0..9] ∈ {0}
l1 ∈ {0}
l2 ∈ {0}
l3 ∈ {0}
pl ∈ {0}
Tm1[0] ∈ {{ &a }}
[1] ∈ {{ &b }}
Tm2[0] ∈ {{ &a }}
[1] ∈ {{ &b }}
Tm3[0] ∈ {{ &a }}
[1] ∈ {{ &b }}
Tm4[0] ∈ {{ &a }}
[1] ∈ {{ &b }}
pm1 ∈ {0}
pm2 ∈ {0}
qm2 ∈ {0}
pun ∈ {0}
pun2 ∈ {0}
qun2 ∈ {0}
random ∈ [--..--]
esc1 ∈ {0}
esc2 ∈ {0}
esc3 ∈ {0}
esc4 ∈ {0}
esc5 ∈ {0}
x ∈ {0}
y ∈ {0}
v.c ∈ {1}
.[bits 8 to 15] ∈ {0}
.i ∈ {2}
.p ∈ {{ &x }}
.t[0] ∈ {{ &y }}
.t[1] ∈ {0}
[value] computing for function f <- origin.
Called from tests/value/origin.i:122.
tests/value/origin.i:122:[kernel] warning: Neither code nor specification for function f, generating default assigns from the prototype
[value] using specification for function f
[value] Done for function f
tests/value/origin.i:124:[value] Assigning imprecise value to r.p.
The imprecision originates from Misaligned {tests/value/origin.i:124}
tests/value/origin.i:127:[value] Assigning imprecise value to r.t[0].
The imprecision originates from Merge {tests/value/origin.i:127}
tests/value/origin.i:128:[value] warning: signed overflow. assert -2147483648 ≤ -((int)(&x));
tests/value/origin.i:128:[value] warning: signed overflow. assert -((int)(&x)) ≤ 2147483647;
tests/value/origin.i:128:[value] Assigning imprecise value to r.t[1].
The imprecision originates from Arithmetic {tests/value/origin.i:128}
[value] Recording results for origin
[value] done for function origin
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function origin:
r.c ∈ [--..--]
.[bits 8 to 15] ∈ UNINITIALIZED
.i ∈ [--..--]
.p ∈
{{ garbled mix of &{x} (origin: Misaligned {tests/value/origin.i:124}) }}
.t[0][bits 0 to 7] ∈
{{ garbled mix of &{y} (origin: Merge {tests/value/origin.i:127}) }}
.t[0][bits 8 to 15]# ∈ {{ NULL ; (? *)&y }}%32, bits 24 to 31
.t[0][bits 16 to 31] ∈ {0}
.t[1] ∈
{{ garbled mix of &{x} (origin: Arithmetic {tests/value/origin.i:128}) }}
q1[bits 0 to 15]# ∈ {{ (? *)&y }}%32, bits 16 to 31
[bits 16 to 31] ∈ {0}
q2[bits 0 to 7] ∈
{{ garbled mix of &{y} (origin: Merge {tests/value/origin.i:127}) }}
[bits 8 to 15]# ∈ {{ NULL ; (? *)&y }}%32, bits 24 to 31
[bits 16 to 31] ∈ {0}
[from] Computing for function origin
[from] Computing for function f <-origin
[from] Done for function f
[from] Done for function origin
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
\result FROM \nothing
[from] Function origin:
\result FROM v{{.i[bits 8 to 15]; .p[bits 0 to 23]};
.t{[0][bits 16 to 31]; [1][bits 0 to 23]}};
c0
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function origin:
r{.c; {.i; .p; .t[0..1]}}; q1; q2
|
