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/symbol_table.h>
24 
25 #include <testing-utils/message.h>
26 
28 {
29  {
30  const bool has_language = get_language_from_mode(ID_C) != nullptr;
31 
32  if(!has_language)
33  {
35  }
36  }
37 
38  {
39  cmdlinet cmdline;
40 
41  config = configt{};
42  config.main = std::string("main");
43  config.set(cmdline);
44  }
45 
46  language_filest language_files;
48 
49  language_filet &language_file = language_files.add_file("");
50 
51  language_file.language = get_language_from_mode(ID_C);
52  CHECK_RETURN(language_file.language);
53 
54  languaget &language = *language_file.language;
56 
57  {
58  const bool error = language.parse(in, "");
59 
60  if(error)
61  throw invalid_source_file_exceptiont("parsing failed");
62  }
63 
64  language_file.get_modules();
65 
66  goto_modelt goto_model;
67 
68  {
69  const bool error = language_files.typecheck(goto_model.symbol_table);
70 
71  if(error)
72  throw invalid_source_file_exceptiont("typechecking failed");
73  }
74 
75  {
76  const bool error =
77  language_files.generate_support_functions(goto_model.symbol_table);
78 
79  if(error)
81  "support function generation failed");
82  }
83 
85  goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
86 
87  return goto_model;
88 }
89 
90 goto_modelt get_goto_model_from_c(const std::string &code)
91 {
92  std::istringstream in(code);
93  return get_goto_model_from_c(in);
94 }
std::unique_ptr< languaget > new_ansi_c_language()
Globally accessible architectural configuration.
Definition: config.h:105
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
optionalt< std::string > main
Definition: config.h:260
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Thrown when we can't handle something in an input source file.
language_filet & add_file(const std::string &filename)
Definition: language_file.h:77
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
bool generate_support_functions(symbol_tablet &symbol_table)
std::unique_ptr< languaget > language
Definition: language_file.h:47
virtual bool parse(std::istream &instream, const std::string &path)=0
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
configt config
Definition: config.cpp:25
goto_modelt get_goto_model_from_c(std::istream &in)
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
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:39
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
Author: Diffblue Ltd.
null_message_handlert null_message_handler
Definition: message.cpp:14