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>
14 
15 #include <iosfwd>
16 
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 &,
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 
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 
66 {
67 public:
73 
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