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
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:120
Properties.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
bool static_verifier(const goto_modelt &, const ai_baset &, const optionst &, message_handlert &, std::ostream &)
Runs the analyzer and then prints out the domain.