CBMC
static_show_domain.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_SHOW_DOMAIN_H
10 #define CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H
11 
12 #include <iosfwd>
13 
14 class ai_baset;
15 class goto_modelt;
16 class optionst;
17 
18 void static_show_domain(
19  const goto_modelt &,
20  const ai_baset &,
21  const optionst &,
22  std::ostream &);
23 
24 #endif // CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:117
goto_modelt
Definition: goto_model.h:27
static_show_domain
void static_show_domain(const goto_modelt &, const ai_baset &, const optionst &, std::ostream &)
Runs the analyzer and then prints out the domain.
Definition: static_show_domain.cpp:21