cprover
get_goto_model_from_c.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Get goto model
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
10 
11 #include <ansi-c/ansi_c_language.h>
12 
14 
15 #include <langapi/language_file.h>
16 #include <langapi/mode.h>
17 
18 #include <util/cmdline.h>
19 #include <util/config.h>
20 #include <util/exception_utils.h>
21 #include <util/invariant.h>
22 #include <util/message.h>
23 #include <util/options.h>
24 #include <util/symbol_table.h>
25 
26 #include <testing-utils/message.h>
27 
29 {
30  {
31  const bool has_language = get_language_from_mode(ID_C) != nullptr;
32 
33  if(!has_language)
34  {
36  }
37  }
38 
39  {
40  cmdlinet cmdline;
41 
42  config = configt{};
43  config.main = std::string("main");
44  config.set(cmdline);
45  }
46 
47  language_filest language_files;
49 
50  language_filet &language_file = language_files.add_file("");
51 
52  language_file.language = get_language_from_mode(ID_C);
53  CHECK_RETURN(language_file.language);
54 
55  languaget &language = *language_file.language;
57 
58  {
59  const bool error = language.parse(in, "");
60 
61  if(error)
62  throw invalid_source_file_exceptiont("parsing failed");
63  }
64 
65  language_file.get_modules();
66 
67  goto_modelt goto_model;
68 
69  {
70  const bool error = language_files.typecheck(goto_model.symbol_table);
71 
72  if(error)
73  throw invalid_source_file_exceptiont("typechecking failed");
74  }
75 
76  {
77  const bool error =
78  language_files.generate_support_functions(goto_model.symbol_table);
79 
80  if(error)
82  "support function generation failed");
83  }
84 
86  goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
87 
88  return goto_model;
89 }
90 
91 goto_modelt get_goto_model_from_c(const std::string &code)
92 {
93  std::istringstream in(code);
94  return get_goto_model_from_c(in);
95 }
exception_utils.h
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:35
get_goto_model_from_c
goto_modelt get_goto_model_from_c(std::istream &in)
Definition: get_goto_model_from_c.cpp:28
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:85
language_filet
Definition: language_file.h:41
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
configt::main
optionalt< std::string > main
Definition: config.h:181
invariant.h
goto_modelt
Definition: goto_model.h:26
mode.h
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
options.h
Options.
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:165
configt
Globally accessible architectural configuration.
Definition: config.h:26
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1846
message.h
cmdlinet
Definition: cmdline.h:21
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
language_filest::add_file
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
config
configt config
Definition: config.cpp:24
get_goto_model_from_c.h
register_language
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:38
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
ansi_c_language.h
cmdline.h
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
languaget
Definition: language.h:40
config.h
goto_convert_functions.h
Goto Programs with Functions.
symbol_table.h
Author: Diffblue Ltd.
message.h
null_message_handler
null_message_handlert null_message_handler
Definition: message.cpp:14
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
language_file.h
language_filest
Definition: language_file.h:62