CBMC
Loading...
Searching...
No Matches
static_verifier.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: goto-analyzer
4
5Author: 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
19class ai_baset;
20class goto_modelt;
22class optionst;
23
25 const goto_modelt &,
26 const ai_baset &,
27 const optionst &,
29 std::ostream &);
30
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
59std::string as_string(const ai_verifier_statust &);
60
84
85#endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
Abstract Interpretation history.
Abstract interface to eager or lazy GOTO models.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
std::set< trace_ptrt, compare_historyt > trace_sett
Definition ai_history.h:79
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
instructionst::const_iterator const_targett
Definition json.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The result of verifying a single assertion As well as the status of the assertion (see above),...
ai_verifier_statust status
jsont output_json(void) const
source_locationt source_location
ai_history_baset::trace_sett unknown_histories
ai_history_baset::trace_sett false_histories
xmlt output_xml(void) const
Definition xml.h:21
Properties.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
std::string as_string(const ai_verifier_statust &)
Makes a status message string from a status.
ai_verifier_statust
An ai_baset contains zero or more histories that reach a location.
bool static_verifier(const goto_modelt &, const ai_baset &, const optionst &, message_handlert &, std::ostream &)
Runs the analyzer and then prints out the domain.