CBMC
static_simplifier.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_SIMPLIFIER_H
10 #define CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H
11 
12 #include <iosfwd>
13 
14 class ai_baset;
15 class goto_modelt;
16 class message_handlert;
17 class optionst;
18 
19 bool static_simplifier(
20  goto_modelt &,
21  const ai_baset &,
22  const optionst &,
23  message_handlert &,
24  std::ostream &);
25 
26 #endif // CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_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
message_handlert
Definition: message.h:27
static_simplifier
bool static_simplifier(goto_modelt &, const ai_baset &, const optionst &, message_handlert &, std::ostream &)
Simplifies the program using the information in the abstract domain.
Definition: static_simplifier.cpp:29