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 <
analyses/ai.h
>
13
#include <
goto-checker/properties.h
>
14
15
#include <iosfwd>
16
17
class
abstract_goto_modelt
;
18
class
ai_baset
;
19
class
goto_modelt
;
20
class
message_handlert
;
21
class
optionst
;
22
23
bool
static_verifier
(
24
const
goto_modelt
&,
25
const
ai_baset
&,
26
const
optionst
&,
27
message_handlert
&,
28
std::ostream &);
29
36
void
static_verifier
(
37
const
abstract_goto_modelt
&abstract_goto_model,
38
const
ai_baset
&ai,
39
propertiest
&properties);
40
50
enum class
ai_verifier_statust
51
{
52
TRUE
,
// true : 1+, unknown : 0, false : 0
53
FALSE_IF_REACHABLE,
// true : 0+, unknown : 0, false : 1+
54
NOT_REACHABLE,
// true : 0, unknown : 0, false : 0
55
UNKNOWN
// true : 0+, unknown : 1+, false : 0+
56
};
57
58
std::string
as_string
(
const
ai_verifier_statust
&);
59
65
class
static_verifier_resultt
66
{
67
public
:
68
ai_verifier_statust
status
;
69
source_locationt
source_location
;
70
irep_idt
function_id
;
71
ai_history_baset::trace_sett
unknown_histories
;
72
ai_history_baset::trace_sett
false_histories
;
73
74
static_verifier_resultt
(
75
const
ai_baset
&ai,
76
goto_programt::const_targett
assert_location,
77
irep_idt
func_id,
78
const
namespacet
&ns);
79
80
jsont
output_json
(
void
)
const
;
81
xmlt
output_xml
(
void
)
const
;
82
};
83
84
#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:407
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition:
properties.h:75
ai_verifier_statust::UNKNOWN
@ UNKNOWN
optionst
Definition:
options.h:23
as_string
std::string as_string(const ai_verifier_statust &)
Makes a status message string from a status.
Definition:
static_verifier.cpp:23
goto_modelt
Definition:
goto_model.h:26
jsont
Definition:
json.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
ai_history_baset::trace_sett
std::set< trace_ptrt, compare_historyt > trace_sett
Definition:
ai_history.h:79
static_verifier_resultt::unknown_histories
ai_history_baset::trace_sett unknown_histories
Definition:
static_verifier.h:71
static_verifier_resultt
The result of verifying a single assertion As well as the status of the assertion (see above),...
Definition:
static_verifier.h:66
ai_verifier_statust::TRUE
@ TRUE
message_handlert
Definition:
message.h:28
static_verifier_resultt::source_location
source_locationt source_location
Definition:
static_verifier.h:69
ai.h
Abstract Interpretation.
xmlt
Definition:
xml.h:21
source_locationt
Definition:
source_location.h:20
static_verifier_resultt::function_id
irep_idt function_id
Definition:
static_verifier.h:70
ai_verifier_statust
ai_verifier_statust
An ai_baset contains zero or more histories that reach a location.
Definition:
static_verifier.h:51
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition:
ai.h:120
static_verifier_resultt::false_histories
ai_history_baset::trace_sett false_histories
Definition:
static_verifier.h:72
static_verifier_resultt::output_json
jsont output_json(void) const
Definition:
static_verifier.cpp:39
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition:
goto_program.h:564
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition:
abstract_goto_model.h:21
properties.h
Properties.
static_verifier_resultt::status
ai_verifier_statust status
Definition:
static_verifier.h:68
static_verifier_resultt::static_verifier_resultt
static_verifier_resultt(const ai_baset &ai, goto_programt::const_targett assert_location, irep_idt func_id, const namespacet &ns)
Definition:
static_verifier.cpp:111
static_verifier_resultt::output_xml
xmlt output_xml(void) const
Definition:
static_verifier.cpp:57
goto-analyzer
static_verifier.h
Generated by
1.8.20