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;
48
49 language_filet &language_file = language_files.add_file("");
50
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
90goto_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()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Globally accessible architectural configuration.
Definition config.h:104
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
optionalt< std::string > main
Definition config.h:326
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.
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
language_filet & add_file(const std::string &filename)
bool generate_support_functions(symbol_tablet &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
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.
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