cprover
static_verifier.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: goto-analyzer
4
5
Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7
\*******************************************************************/
8
9
#ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
10
#define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
11
12
#include <
goto-checker/properties.h
>
13
#include <iosfwd>
14
15
class
abstract_goto_modelt
;
16
class
ai_baset
;
17
class
goto_modelt
;
18
class
message_handlert
;
19
class
optionst
;
20
21
bool
static_verifier
(
22
const
goto_modelt
&,
23
const
ai_baset
&,
24
const
optionst
&,
25
message_handlert
&,
26
std::ostream &);
27
34
void
static_verifier
(
35
const
abstract_goto_modelt
&abstract_goto_model,
36
const
ai_baset
&ai,
37
propertiest
&properties);
38
39
#endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
static_verifier
bool static_verifier(const goto_modelt &, const ai_baset &, const optionst &, message_handlert &, std::ostream &)
Runs the analyzer and then prints out the domain.
Definition:
static_verifier.cpp:297
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition:
properties.h:75
optionst
Definition:
options.h:23
goto_modelt
Definition:
goto_model.h:26
message_handlert
Definition:
message.h:28
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition:
ai.h:119
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition:
abstract_goto_model.h:21
properties.h
Properties.
goto-analyzer
static_verifier.h
Generated by
1.8.20