CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
11#include <util/cmdline.h>
12#include <util/config.h>
14#include <util/invariant.h>
15#include <util/message.h>
16#include <util/symbol_table.h>
17
21#include <langapi/mode.h>
23
25{
26 {
27 const bool has_language = get_language_from_mode(ID_C) != nullptr;
28
29 if(!has_language)
30 {
32 }
33 }
34
35 {
36 cmdlinet cmdline;
37
38 config = configt{};
39 config.main = std::string("main");
40 config.set(cmdline);
41 }
42
43 language_filest language_files;
44
45 language_filet &language_file = language_files.add_file("");
46
49
50 languaget &language = *language_file.language;
51
52 {
53 const bool error = language.parse(in, "", null_message_handler);
54
55 if(error)
56 throw invalid_input_exceptiont("parsing failed");
57 }
58
59 language_file.get_modules();
60
61 goto_modelt goto_model;
62
63 {
64 const bool error =
65 language_files.typecheck(goto_model.symbol_table, null_message_handler);
66
67 if(error)
68 throw invalid_input_exceptiont("typechecking failed");
69 }
70
71 {
72 const bool error = language_files.generate_support_functions(
74
75 if(error)
76 throw invalid_input_exceptiont("support function generation failed");
77 }
78
80 goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
81
82 return goto_model;
83}
84
85goto_modelt get_goto_model_from_c(const std::string &code)
86{
87 std::istringstream in(code);
88 return get_goto_model_from_c(in);
89}
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:562
Globally accessible architectural configuration.
Definition config.h:138
bool set(const cmdlinet &cmdline)
Definition config.cpp:863
std::optional< std::string > main
Definition config.h:372
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)
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)
language_filet & add_file(const std::string &filename)
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
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