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 
13 #include <iosfwd>
14 
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 &,
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.