File tree Expand file tree Collapse file tree 1 file changed +25
-25
lines changed Expand file tree Collapse file tree 1 file changed +25
-25
lines changed Original file line number Diff line number Diff line change @@ -27,6 +27,31 @@ struct static_verifier_resultt
27
27
irep_idt function_id;
28
28
};
29
29
30
+ static static_verifier_resultt::statust
31
+ check_assertion (const ai_domain_baset &domain, exprt e, const namespacet &ns)
32
+ {
33
+ if (domain.is_bottom ())
34
+ {
35
+ return static_verifier_resultt::BOTTOM;
36
+ }
37
+
38
+ domain.ai_simplify (e, ns);
39
+ if (e.is_true ())
40
+ {
41
+ return static_verifier_resultt::TRUE ;
42
+ }
43
+ else if (e.is_false ())
44
+ {
45
+ return static_verifier_resultt::FALSE ;
46
+ }
47
+ else
48
+ {
49
+ return static_verifier_resultt::UNKNOWN;
50
+ }
51
+
52
+ UNREACHABLE;
53
+ }
54
+
30
55
void static_verifier (
31
56
const abstract_goto_modelt &abstract_goto_model,
32
57
const ai_baset &ai,
@@ -224,31 +249,6 @@ static void static_verifier_console(
224
249
m.result () << ' \n ' ;
225
250
}
226
251
227
- static static_verifier_resultt::statust
228
- check_assertion (const ai_domain_baset &domain, exprt e, const namespacet &ns)
229
- {
230
- if (domain.is_bottom ())
231
- {
232
- return static_verifier_resultt::BOTTOM;
233
- }
234
-
235
- domain.ai_simplify (e, ns);
236
- if (e.is_true ())
237
- {
238
- return static_verifier_resultt::TRUE ;
239
- }
240
- else if (e.is_false ())
241
- {
242
- return static_verifier_resultt::FALSE ;
243
- }
244
- else
245
- {
246
- return static_verifier_resultt::UNKNOWN;
247
- }
248
-
249
- UNREACHABLE;
250
- }
251
-
252
252
// / Runs the analyzer and then prints out the domain
253
253
// / \param goto_model: the program analyzed
254
254
// / \param ai: the abstract interpreter after it has been run to fix point
You can’t perform that action at this time.
0 commit comments