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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/logic.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
t[0..9] ∈ {0}
u[0..10] ∈ {0}
s1 ∈ {0}
s2 ∈ {0}
s3[0..9] ∈ {0}
x ∈ {0}
v ∈ [--..--]
[value] computing for function eq_tsets <- main.
Called from tests/value/logic.c:115.
tests/value/logic.c:7:[value] cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#2>
tests/value/logic.c:7:[value] warning: assertion got status unknown.
tests/value/logic.c:9:[value] assertion got status valid.
tests/value/logic.c:10:[value] warning: assertion got status unknown.
tests/value/logic.c:11:[value] warning: assertion got status unknown.
tests/value/logic.c:12:[value] warning: assertion got status unknown.
tests/value/logic.c:13:[value] warning: assertion got status unknown.
tests/value/logic.c:14:[value] assertion got status valid.
tests/value/logic.c:15:[value] warning: assertion got status unknown.
tests/value/logic.c:16:[value] warning: assertion got status unknown.
tests/value/logic.c:17:[value] assertion got status valid.
tests/value/logic.c:19:[value] assertion got status valid.
tests/value/logic.c:21:[value] assertion got status valid.
tests/value/logic.c:23:[value] assertion got status valid.
tests/value/logic.c:24:[value] warning: assertion got status unknown.
tests/value/logic.c:25:[value] assertion got status valid.
tests/value/logic.c:26:[value] warning: assertion got status unknown.
tests/value/logic.c:29:[value] warning: assertion got status unknown.
tests/value/logic.c:30:[value] warning: assertion got status unknown.
tests/value/logic.c:31:[value] warning: assertion got status unknown.
tests/value/logic.c:32:[value] assertion got status valid.
tests/value/logic.c:34:[value] assertion got status valid.
tests/value/logic.c:35:[value] assertion got status valid.
tests/value/logic.c:36:[value] warning: assertion got status unknown.
tests/value/logic.c:38:[value] cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type struct ts
tests/value/logic.c:38:[value] warning: assertion got status unknown.
tests/value/logic.c:39:[value] cannot evaluate ACSL term, unsupported ACSL construct: != operation on non-supported type int [10]
tests/value/logic.c:39:[value] warning: assertion got status unknown.
tests/value/logic.c:41:[value] assertion got status valid.
tests/value/logic.c:42:[value] assertion got status valid.
tests/value/logic.c:43:[value] assertion got status valid.
tests/value/logic.c:45:[value] assertion got status valid.
tests/value/logic.c:47:[value] cannot evaluate ACSL term, unsupported ACSL construct: set intersection
tests/value/logic.c:47:[value] warning: assertion got status unknown.
[value] Recording results for eq_tsets
[value] Done for function eq_tsets
[value] computing for function eq_char <- main.
Called from tests/value/logic.c:116.
[value] Called Frama_C_show_each({-126})
tests/value/logic.c:54:[value] assertion got status valid.
tests/value/logic.c:55:[value] assertion got status valid.
[value] Recording results for eq_char
[value] Done for function eq_char
[value] computing for function casts <- main.
Called from tests/value/logic.c:117.
tests/value/logic.c:59:[value] assertion got status valid.
tests/value/logic.c:60:[value] assertion got status valid.
[value] Recording results for casts
[value] Done for function casts
[value] computing for function empty_tset <- main.
Called from tests/value/logic.c:118.
[value] computing for function f_empty_tset <- empty_tset <- main.
Called from tests/value/logic.c:70.
[value] using specification for function f_empty_tset
tests/value/logic.c:63:[value] function f_empty_tset: precondition 'r1' got status valid.
tests/value/logic.c:64:[value] function f_empty_tset: precondition 'r2' got status valid.
[value] Done for function f_empty_tset
tests/value/logic.c:71:[value] assertion got status valid.
[value] Recording results for empty_tset
[value] Done for function empty_tset
[value] computing for function reduce_by_equal <- main.
Called from tests/value/logic.c:119.
tests/value/logic.c:76:[value] warning: accessing out of bounds index. assert 0 ≤ v;
tests/value/logic.c:76:[value] warning: accessing out of bounds index. assert v < 10;
tests/value/logic.c:77:[value] warning: assertion got status unknown.
tests/value/logic.c:78:[value] warning: assertion got status unknown.
[value] Recording results for reduce_by_equal
[value] Done for function reduce_by_equal
[value] computing for function alarms <- main.
Called from tests/value/logic.c:120.
tests/value/logic.c:86:[value] warning: assertion 'ASSUME' got status unknown.
tests/value/logic.c:88:[value] warning: assertion 'UNK' got status unknown.
[value] Called Frama_C_show_each({-1; 1})
tests/value/logic.c:90:[value] warning: assertion 'UNK' got status unknown.
[value] Called Frama_C_show_each({-1; 1})
tests/value/logic.c:93:[value] warning: assertion 'ASSUME' got status unknown.
tests/value/logic.c:94:[value] assertion 'OK' got status valid.
[value] Called Frama_C_show_each({1})
tests/value/logic.c:96:[value] assertion 'OK' got status valid.
[value] Called Frama_C_show_each({1})
tests/value/logic.c:101:[value] warning: assertion 'ASSUME' got status unknown.
tests/value/logic.c:102:[value] warning: assertion 'UNK' got status unknown.
[value] Called Frama_C_show_each({0; 1})
tests/value/logic.c:104:[value] warning: assertion 'UNK' got status unknown.
[value] Called Frama_C_show_each({0; 1})
tests/value/logic.c:107:[value] warning: assertion 'ASSUME' got status unknown.
tests/value/logic.c:108:[value] assertion 'OK' got status valid.
[value] Called Frama_C_show_each({1})
tests/value/logic.c:110:[value] assertion 'OK' got status valid.
[value] Called Frama_C_show_each({1})
[value] Recording results for alarms
[value] Done for function alarms
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function alarms:
x_0 ∈ {1}
[value:final-states] Values at end of function casts:
[value:final-states] Values at end of function eq_char:
c ∈ {-126}
[value:final-states] Values at end of function eq_tsets:
[value:final-states] Values at end of function empty_tset:
T[0] ∈ {2}
[value:final-states] Values at end of function reduce_by_equal:
a[0..8] ∈ {1}
[9] ∈ [--..--]
[value:final-states] Values at end of function main:
[from] Computing for function alarms
[from] Done for function alarms
[from] Computing for function casts
[from] Done for function casts
[from] Computing for function eq_char
[from] Done for function eq_char
[from] Computing for function eq_tsets
[from] Done for function eq_tsets
[from] Computing for function empty_tset
[from] Computing for function f_empty_tset <-empty_tset
[from] Done for function f_empty_tset
[from] Done for function empty_tset
[from] Computing for function reduce_by_equal
[from] Done for function reduce_by_equal
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function alarms:
NO EFFECTS
[from] Function casts:
NO EFFECTS
[from] Function eq_char:
NO EFFECTS
[from] Function eq_tsets:
NO EFFECTS
[from] Function f_empty_tset:
NO EFFECTS
[from] Function empty_tset:
NO EFFECTS
[from] Function reduce_by_equal:
NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function alarms:
x_0
[inout] Inputs for function alarms:
v
[inout] Out (internal) for function casts:
\nothing
[inout] Inputs for function casts:
\nothing
[inout] Out (internal) for function eq_char:
c
[inout] Inputs for function eq_char:
\nothing
[inout] Out (internal) for function eq_tsets:
\nothing
[inout] Inputs for function eq_tsets:
\nothing
[inout] Out (internal) for function empty_tset:
T[0]
[inout] Inputs for function empty_tset:
\nothing
[inout] Out (internal) for function reduce_by_equal:
a[0..9]
[inout] Inputs for function reduce_by_equal:
v
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
v
|
