cprover
Loading...
Searching...
No Matches
get_goto_model_from_c.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Get goto model
4
5Author: Daniel Poetzl
6
7\*******************************************************************/
8
10
12
14
16#include <langapi/mode.h>
17
18#include <util/cmdline.h>
19#include <util/config.h>
21#include <util/invariant.h>
22#include <util/message.h>
23#include <util/symbol_table.h>
24
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;
47
48 language_filet &language_file = language_files.add_file("");
49
52
53 languaget &language = *language_file.language;
55
56 {
57 const bool error = language.parse(in, "");
58
59 if(error)
60 throw invalid_input_exceptiont("parsing failed");
61 }
62
63 language_file.get_modules();
64
65 goto_modelt goto_model;
66
67 {
68 const bool error =
69 language_files.typecheck(goto_model.symbol_table, null_message_handler);
70
71 if(error)
72 throw invalid_input_exceptiont("typechecking failed");
73 }
74
75 {
76 const bool error =
77 language_files.generate_support_functions(goto_model.symbol_table);
78
79 if(error)
80 throw invalid_input_exceptiont("support function generation failed");
81 }
82
84 goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
85
86 return goto_model;
87}
88
89goto_modelt get_goto_model_from_c(const std::string &code)
90{
91 std::istringstream in(code);
92 return get_goto_model_from_c(in);
93}
std::unique_ptr< languaget > new_ansi_c_language()
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Globally accessible architectural configuration.
Definition config.h:129
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
optionalt< std::string > main
Definition config.h:353
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
Thrown when user-provided input cannot be processed.
bool typecheck(symbol_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
language_filet & add_file(const std::string &filename)
bool generate_support_functions(symbol_table_baset &symbol_table)
virtual bool parse(std::istream &instream, const std::string &path)=0
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
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.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition mode.cpp:51
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
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
Author: Diffblue Ltd.
null_message_handlert null_message_handler
Definition message.cpp:14