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
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/precond.c (with preprocessing)
[value] Analyzing an incomplete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
x ∈ [--..--]
pf2 ∈ {{ &f2 }}
[value] computing for function f <- main.
Called from tests/value/precond.c:31.
tests/value/precond.c:8:[value] function f: precondition got status valid.
tests/value/precond.c:9:[value] function f: precondition got status valid.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
Called from tests/value/precond.c:32.
[value] Recording results for f
[value] Done for function f
[value] computing for function g <- main.
Called from tests/value/precond.c:34.
tests/value/precond.c:34:[kernel] warning: No code nor implicit assigns clause for function g, generating default assigns from the prototype
[value] using specification for function g
tests/value/precond.c:24:[value] warning: function g: precondition got status unknown.
[value] Done for function g
[value] computing for function aux <- main.
Called from tests/value/precond.c:36.
[value] computing for function f2 <- aux <- main.
Called from tests/value/precond.c:21.
tests/value/precond.c:21:[kernel] warning: No code nor implicit assigns clause for function f2, generating default assigns from the prototype
[value] using specification for function f2
tests/value/precond.c:15:[value] function f2: precondition got status valid.
[value] Done for function f2
[value] Recording results for aux
[value] Done for function aux
[value] computing for function aux <- main.
Called from tests/value/precond.c:37.
[value] computing for function f2 <- aux <- main.
Called from tests/value/precond.c:21.
tests/value/precond.c:15:[value] warning: function f2: precondition got status unknown.
[value] Done for function f2
[value] Recording results for aux
[value] Done for function aux
[value] computing for function f <- main.
Called from tests/value/precond.c:39.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
Called from tests/value/precond.c:40.
tests/value/precond.c:9:[value] warning: function f: precondition got status invalid.
[value] Recording results for f
[value] Done for function f
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function f:
x ∈ {0; 1}
[value:final-states] Values at end of function aux:
[value:final-states] Values at end of function main:
NON TERMINATING FUNCTION
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ Valid ] Pre-condition (file tests/value/precond.c, line 8)
requires i + 1 ≥ 0
by Call Preconditions.
[ Alarm ] Pre-condition (file tests/value/precond.c, line 9)
requires i ≥ 0
By Call Preconditions, with pending:
- Unreachable instruction (file tests/value/precond.c, line 40)
--------------------------------------------------------------------------------
--- Properties of Function 'f2'
--------------------------------------------------------------------------------
[ - ] Pre-condition (file tests/value/precond.c, line 15)
requires i ≥ 0
tried with Call Preconditions.
[ - ] Assigns nothing
assigns \nothing;
tried with Inferred annotations.
[ - ] Default behavior
default behavior
tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'aux'
--------------------------------------------------------------------------------
[ - ] Instance of 'Pre-condition (file tests/value/precond.c, line 15)' at instruction (file tests/value/precond.c, line 21)
status of 'requires i ≥ 0' of f2 at stmt 4
tried with Value.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
[ - ] Pre-condition (file tests/value/precond.c, line 24)
requires x ≤ 8
tried with Call Preconditions.
[ - ] Assigns nothing
assigns \nothing;
tried with Inferred annotations.
[ - ] Default behavior
default behavior
tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 8)' at call 'f' (file tests/value/precond.c, line 31)
status of 'requires i + 1 ≥ 0' of f at stmt 11
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 9)' at call 'f' (file tests/value/precond.c, line 31)
status of 'requires i ≥ 0' of f at stmt 11
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 8)' at call 'f' (file tests/value/precond.c, line 32)
status of 'requires i + 1 ≥ 0' of f at stmt 14
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 9)' at call 'f' (file tests/value/precond.c, line 32)
status of 'requires i ≥ 0' of f at stmt 14
by Value.
[ - ] Instance of 'Pre-condition (file tests/value/precond.c, line 24)' at call 'g' (file tests/value/precond.c, line 34)
status of 'requires x ≤ 8' of g at stmt 17
tried with Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 8)' at instruction (file tests/value/precond.c, line 39)
status of 'requires i + 1 ≥ 0' of f at stmt 20
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 9)' at instruction (file tests/value/precond.c, line 39)
status of 'requires i ≥ 0' of f at stmt 20
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/precond.c, line 8)' at instruction (file tests/value/precond.c, line 40)
status of 'requires i + 1 ≥ 0' of f at stmt 21
by Value.
[ Alarm ] Instance of 'Pre-condition (file tests/value/precond.c, line 9)' at instruction (file tests/value/precond.c, line 40)
status of 'requires i ≥ 0' of f at stmt 21
By Value, with pending:
- Unreachable instruction (file tests/value/precond.c, line 40)
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
8 Completely validated
8 To be validated
2 Alarms emitted
18 Total
--------------------------------------------------------------------------------
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ Valid ] Pre-condition (file tests/value/precond.c, line 8)
requires i + 1 ≥ 0
by Call Preconditions.
[ Alarm ] Pre-condition (file tests/value/precond.c, line 9)
requires i ≥ 0
By Call Preconditions, with pending:
- Unreachable instruction (file tests/value/precond.c, line 40)
--------------------------------------------------------------------------------
--- Properties of Function 'f2'
--------------------------------------------------------------------------------
[ - ] Pre-condition (file tests/value/precond.c, line 15)
requires i ≥ 0
tried with Call Preconditions.
[ - ] Assigns nothing
assigns \nothing;
tried with Inferred annotations.
[ - ] Default behavior
default behavior
tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'g'
--------------------------------------------------------------------------------
[ - ] Pre-condition (file tests/value/precond.c, line 24)
requires x ≤ 8
tried with Call Preconditions.
[ - ] Assigns nothing
assigns \nothing;
tried with Inferred annotations.
[ - ] Default behavior
default behavior
tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
1 Completely validated
6 To be validated
1 Alarm emitted
8 Total
--------------------------------------------------------------------------------
|
