CBMC
initialize_goto_model.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Initialize a Goto Program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
13 #define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
14 
15 #include "goto_model.h"
16 
17 class language_filest;
18 class message_handlert;
19 class optionst;
20 
21 goto_modelt initialize_goto_model(
22  const std::vector<std::string> &files,
23  message_handlert &message_handler,
24  const optionst &options);
25 
34 void initialize_from_source_files(
35  const std::list<std::string> &sources,
36  const optionst &options,
37  language_filest &language_files,
38  symbol_tablet &symbol_table,
39  message_handlert &message_handler);
40 
51 void set_up_custom_entry_point(
52  language_filest &language_files,
53  symbol_tablet &symbol_table,
54  const std::function<std::size_t(const irep_idt &)> &unload,
55  const optionst &options,
56  bool try_mode_lookup,
57  message_handlert &message_handler);
58 
59 #endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
goto_modelt
Definition: goto_model.h:27
language_filest
Definition: language_file.h:63
message_handlert
Definition: message.h:28
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
goto_model.h
Symbol Table + CFG.
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:172
initialize_from_source_files
void initialize_from_source_files(const std::list< std::string > &sources, const optionst &options, language_filest &language_files, symbol_tablet &symbol_table, message_handlert &message_handler)
Populate symbol_table from sources by parsing and type checking via language_files.
Definition: initialize_goto_model.cpp:60
set_up_custom_entry_point
void set_up_custom_entry_point(language_filest &language_files, symbol_tablet &symbol_table, const std::function< std::size_t(const irep_idt &)> &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler)
Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.
Definition: initialize_goto_model.cpp:111