CBMC
build_analyzer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyzer Command Line Option Processing
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_ANALYZER_BUILD_ANALYZER_H
10 #define CPROVER_GOTO_ANALYZER_BUILD_ANALYZER_H
11 
12 #include <memory>
13 
14 class ai_baset;
15 class goto_modelt;
16 class namespacet;
17 class optionst;
18 class message_handlert;
19 
30 std::unique_ptr<ai_baset> build_analyzer(
31  const optionst &options,
32  const goto_modelt &goto_model,
33  const namespacet &ns,
34  message_handlert &mh);
35 
36 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
build_analyzer
std::unique_ptr< ai_baset > build_analyzer(const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
Build an abstract interpreter configured by the options.
Definition: build_analyzer.cpp:29
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
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94