CBMC
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 
13 
14 #include <iosfwd>
15 
16 #include <analyses/ai_history.h>
17 
19 class ai_baset;
20 class goto_modelt;
21 class message_handlert;
22 class optionst;
23 
24 bool static_verifier(
25  const goto_modelt &,
26  const ai_baset &,
27  const optionst &,
29  std::ostream &);
30 
37 void static_verifier(
38  const abstract_goto_modelt &abstract_goto_model,
39  const ai_baset &ai,
40  propertiest &properties);
41 
52 {
53  TRUE, // true : 1+, unknown : 0, false : 0
54  FALSE_IF_REACHABLE, // true : 0+, unknown : 0, false : 1+
55  NOT_REACHABLE, // true : 0, unknown : 0, false : 0
56  UNKNOWN // true : 0+, unknown : 1+, false : 0+
57 };
58 
59 std::string as_string(const ai_verifier_statust &);
60 
67 {
68 public:
74 
76  const ai_baset &ai,
77  goto_programt::const_targett assert_location,
78  irep_idt func_id,
79  const namespacet &ns);
80 
81  jsont output_json(void) const;
82  xmlt output_xml(void) const;
83 };
84 
85 #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:403
ai_verifier_statust::FALSE_IF_REACHABLE
@ FALSE_IF_REACHABLE
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
ai_verifier_statust::UNKNOWN
@ UNKNOWN
optionst
Definition: options.h:22
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:25
propertiest
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
jsont
Definition: json.h:26
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
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:72
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:27
static_verifier_resultt::source_location
source_locationt source_location
Definition: static_verifier.h:70
xmlt
Definition: xml.h:20
source_locationt
Definition: source_location.h:18
ai_history.h
static_verifier_resultt::function_id
irep_idt function_id
Definition: static_verifier.h:71
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:118
static_verifier_resultt::false_histories
ai_history_baset::trace_sett false_histories
Definition: static_verifier.h:73
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:587
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:20
properties.h
static_verifier_resultt::status
ai_verifier_statust status
Definition: static_verifier.h:69
ai_verifier_statust::NOT_REACHABLE
@ NOT_REACHABLE
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