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
103
104
105
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/div.i (no preprocessing)
[rte] annotating function main
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
X ∈ {0}
Y ∈ {0}
Z1 ∈ {0}
Z2 ∈ {0}
T ∈ {0}
U1 ∈ {0}
U2 ∈ {0}
V ∈ {0}
W1 ∈ {0}
W2 ∈ {0}
a ∈ {0}
b ∈ {0}
d1 ∈ {0}
d2 ∈ {0}
d0 ∈ {0}
e ∈ {0}
t[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3..4] ∈ {0}
p ∈ {0}
tests/value/div.i:14:[value] entering loop for the first time
tests/value/div.i:14:[value] warning: assertion 'rte,signed_overflow' got status unknown.
tests/value/div.i:14:[value] warning: signed overflow. assert c + 1 ≤ 2147483647;
tests/value/div.i:16:[value] assertion 'rte,signed_overflow' got status valid.
tests/value/div.i:17:[value] warning: assertion 'rte,signed_overflow' got status unknown.
tests/value/div.i:17:[value] warning: signed overflow. assert c + 2 ≤ 2147483647;
tests/value/div.i:17:[value] assertion 'rte,signed_overflow' got status valid.
tests/value/div.i:17:[value] warning: assertion 'rte,signed_overflow' got status unknown.
tests/value/div.i:17:[value] warning: signed overflow. assert -2147483648 ≤ X - 1;
tests/value/div.i:16:[value] warning: assertion 'rte,signed_overflow' got status unknown.
tests/value/div.i:16:[value] warning: signed overflow. assert X + 1 ≤ 2147483647;
tests/value/div.i:22:[value] assertion 'rte,signed_overflow' got status valid.
tests/value/div.i:25:[value] assertion 'rte,signed_overflow' got status valid.
tests/value/div.i:28:[value] assertion 'rte,signed_overflow' got status valid.
tests/value/div.i:32:[value] warning: assertion 'rte,division_by_zero' got status unknown.
tests/value/div.i:32:[value] warning: division by zero. assert Z2 ≢ 0;
tests/value/div.i:33:[value] warning: assertion 'rte,division_by_zero' got status unknown.
tests/value/div.i:33:[value] warning: assertion 'rte,signed_overflow' got status unknown.
tests/value/div.i:33:[value] warning: division by zero. assert Z2 ≢ 0;
tests/value/div.i:33:[value] warning: signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
tests/value/div.i:33:[value] warning: signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
tests/value/div.i:33:[value] Assigning imprecise value to b.
The imprecision originates from Arithmetic {tests/value/div.i:33}
tests/value/div.i:34:[value] assertion 'rte,division_by_zero' got status valid.
tests/value/div.i:34:[value] warning: division by zero. assert (int)(&X + 2) ≢ 0;
tests/value/div.i:34:[value] warning: pointer comparison. assert \pointer_comparable((void *)0, (void *)(&X + 2));
tests/value/div.i:34:[value] warning: signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 2);
tests/value/div.i:34:[value] warning: signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
tests/value/div.i:34:[value] Assigning imprecise value to d2.
The imprecision originates from Arithmetic {tests/value/div.i:34}
tests/value/div.i:35:[value] assertion 'rte,division_by_zero' got status valid.
tests/value/div.i:35:[value] warning: signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
tests/value/div.i:35:[value] warning: signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
tests/value/div.i:35:[value] Assigning imprecise value to d1.
The imprecision originates from Arithmetic {tests/value/div.i:35}
tests/value/div.i:36:[value] assertion 'rte,division_by_zero' got status valid.
tests/value/div.i:36:[value] warning: signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
tests/value/div.i:36:[value] warning: signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
tests/value/div.i:36:[value] Assigning imprecise value to d0.
The imprecision originates from Arithmetic {tests/value/div.i:36}
tests/value/div.i:37:[value] warning: assertion 'rte,signed_overflow' got status unknown.
tests/value/div.i:37:[value] warning: signed overflow. assert -2147483648 ≤ -((int)(&X));
tests/value/div.i:37:[value] warning: signed overflow. assert -((int)(&X)) ≤ 2147483647;
tests/value/div.i:37:[value] Assigning imprecise value to e.
The imprecision originates from Arithmetic {tests/value/div.i:37}
[value] Recording results for main
[value] done for function main
tests/value/div.i:22:[value] assertion 'rte,signed_overflow' got final status valid.
tests/value/div.i:25:[value] assertion 'rte,signed_overflow' got final status valid.
tests/value/div.i:28:[value] assertion 'rte,signed_overflow' got final status valid.
tests/value/div.i:34:[value] assertion 'rte,division_by_zero' got final status valid.
tests/value/div.i:35:[value] assertion 'rte,division_by_zero' got final status valid.
tests/value/div.i:36:[value] assertion 'rte,division_by_zero' got final status valid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
X ∈ [--..--]
Y ∈ [-126..333],9%27
Z1 ∈ [-42..111],3%9
Z2 ∈ [-25..66]
T ∈ [34..493],7%27
U1 ∈ [11..164],2%9
U2 ∈ [6..98]
V ∈ [-125..334],10%27
W1 ∈ [-41..111]
W2 ∈ [-25..66]
a ∈ [-40000..40000]
b ∈
{{ garbled mix of &{Z2} (origin: Arithmetic {tests/value/div.i:33}) }}
d1 ∈
{{ garbled mix of &{X} (origin: Arithmetic {tests/value/div.i:35}) }}
d2 ∈
{{ garbled mix of &{X} (origin: Arithmetic {tests/value/div.i:34}) }}
d0 ∈
{{ garbled mix of &{X} (origin: Arithmetic {tests/value/div.i:36}) }}
e ∈ {{ garbled mix of &{X} (origin: Arithmetic {tests/value/div.i:37}) }}
p ∈ {{ &t[3] }}
c ∈ [--..--]
|
