From 03a4213bffa452baffbb32b7d6bf2a55d4dfd1e5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 1 Dec 2016 16:06:24 +0000 Subject: [PATCH 01/11] Generate stub method for opaque functions Initial commit making a stub function in the GOTO program for any opaque functions (i.e. functions for which we don't have a body). This is done to ensure we can match up the assignments after the opaque function to the return from the opaque function. --- src/util/language.cpp | 85 +++++++++++++++++++++++++++++++++++++++++++ src/util/language.h | 10 +++++ 2 files changed, 95 insertions(+) diff --git a/src/util/language.cpp b/src/util/language.cpp index 4b4a1ba4ae4..ff2eb4858b4 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "language.h" #include "expr.h" +#include +#include /*******************************************************************\ @@ -125,3 +127,86 @@ bool languaget::type_to_name( name=type.pretty(); return false; } + +/*******************************************************************\ + +Function: languaget::generate_opaque_method_stubs + + Inputs: + symbol_table - the symbol table for the program + + Outputs: + + Purpose: When there are opaque methods (e.g. ones where we don't + have a body), we create a stub function in the goto + program and mark it as opaque so the interpreter fills in + appropriate values for it. + +\*******************************************************************/ + +void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) +{ + for(auto &symbol_entry : symbol_table.symbols) + { + if(is_symbol_opaque_function(symbol_entry.second)) + { + symbolt &symbol=symbol_entry.second; + + irep_idt return_symbol_id = generate_opaque_stub_body( + symbol, + symbol_table); + + if(return_symbol_id!=ID_nil) + { + symbol.type.set("opaque_method_capture_symbol", return_symbol_id); + } + } + } +} + +/*******************************************************************\ + +Function: languaget::generate_opaque_stub_body + + Inputs: + symbol - the function symbol which is opaque + symbol_table - the symbol table + + Outputs: The identifier of the return variable. ID_nil if the function + doesn't return anything. + + Purpose: To generate the stub function for the opaque function in + question. The identifier is used in the flag to the interpreter + that the function is opaque. This function should be implemented + in the languages. + +\*******************************************************************/ + +irep_idt languaget::generate_opaque_stub_body( + symbolt &symbol, + symbol_tablet &symbol_table) +{ + return ID_nil; +} + + +/*******************************************************************\ + +Function: languaget::is_symbol_opaque_function + + Inputs: + symbol - the symbol to be checked + + Outputs: True if the symbol is an opaque (e.g. non-bodied) function + + Purpose: To identify if a given symbol is an opaque function and + hence needs to be stubbed + +\*******************************************************************/ + +bool languaget::is_symbol_opaque_function(const symbolt &symbol) +{ + return !symbol.is_type && + symbol.value.id()==ID_nil && + symbol.type.id()==ID_code; +} diff --git a/src/util/language.h b/src/util/language.h index b19615496ec..5f284131a0e 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "message.h" class symbol_tablet; +class symbolt; class exprt; class namespacet; class typet; @@ -114,5 +115,14 @@ class languaget:public messaget languaget() { } virtual ~languaget() { } + +protected: + void generate_opaque_method_stubs(symbol_tablet &symbol_table); + virtual irep_idt generate_opaque_stub_body( + symbolt &symbol, + symbol_tablet &symbol_table); + +private: + bool is_symbol_opaque_function(const symbolt &symbol); }; #endif // CPROVER_UTIL_LANGUAGE_H From 06b36cda4b062f5887f7604ddbbb7be5ff13648f Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 2 Dec 2016 11:01:14 +0000 Subject: [PATCH 02/11] Don't create stub for CPROVER_ functions These were having stubs created but they are not opaque functions. This was because their body gets created after this step. --- src/util/language.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/util/language.cpp b/src/util/language.cpp index ff2eb4858b4..cecc7944f88 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr.h" #include #include +#include +#include /*******************************************************************\ @@ -200,13 +202,20 @@ Function: languaget::is_symbol_opaque_function Outputs: True if the symbol is an opaque (e.g. non-bodied) function Purpose: To identify if a given symbol is an opaque function and - hence needs to be stubbed + hence needs to be stubbed. We explicitly exclude CPROVER + functions, if they have no body it is because we haven't + generated it yet. \*******************************************************************/ bool languaget::is_symbol_opaque_function(const symbolt &symbol) { + // Explictly exclude CPROVER functions since these aren't opaque + std::string variable_id_str(symbol.name.c_str()); + bool is_cprover_function = has_prefix(variable_id_str, CPROVER_PREFIX); + return !symbol.is_type && symbol.value.id()==ID_nil && - symbol.type.id()==ID_code; + symbol.type.id()==ID_code && + !is_cprover_function; } From 4b6e9c926944aa047a4fab87475503f3f9abdfe2 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 2 Dec 2016 12:11:25 +0000 Subject: [PATCH 03/11] Create stub argument identifiers for functions with parameters If opaque functions do not name there parameters, it causes issues later when we try to call the stub functions. This creates dummy symbols and names the parameters in the function type. --- src/util/language.cpp | 69 +++++++++++++++++++++++++++++++++++++++++++ src/util/language.h | 9 +++++- 2 files changed, 77 insertions(+), 1 deletion(-) diff --git a/src/util/language.cpp b/src/util/language.cpp index cecc7944f88..7349b09ed1f 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include /*******************************************************************\ @@ -154,6 +155,8 @@ void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) { symbolt &symbol=symbol_entry.second; + generate_opaque_parameter_symbols(symbol, symbol_table); + irep_idt return_symbol_id = generate_opaque_stub_body( symbol, symbol_table); @@ -191,6 +194,36 @@ irep_idt languaget::generate_opaque_stub_body( return ID_nil; } +/*******************************************************************\ + +Function: languaget::build_stub_parameter_symbol + + Inputs: + function_symbol - the symbol of an opaque function + parameter_index - the index of the parameter within the + the parameter list + parameter_type - the type of the parameter + + Outputs: A named symbol to be added to the symbol table representing + one of the parameters in this opaque function. + + Purpose: To build the parameter symbol and choose its name. This should + be implemented in each language. + +\*******************************************************************/ + +parameter_symbolt languaget::build_stub_parameter_symbol( + const symbolt &function_symbol, + size_t parameter_index, + const typet ¶meter_type) +{ + error() << "language " << id() + << " doesn't implement build_stub_parameter_symbol. " + << "This means cannot use opaque functions." << eom; + + return parameter_symbolt(); +} + /*******************************************************************\ @@ -219,3 +252,39 @@ bool languaget::is_symbol_opaque_function(const symbolt &symbol) symbol.type.id()==ID_code && !is_cprover_function; } + +/*******************************************************************\ + +Function: languaget::generate_opaque_parameter_symbols + + Inputs: + function_symbol - the symbol of an opaque function + symbol_table - the symbol table to add the new parameter + symbols into + + Outputs: + + Purpose: To create stub parameter symbols for each parameter the + function has and assign their IDs into the parameters + identifier. + +\*******************************************************************/ + +void languaget::generate_opaque_parameter_symbols( + symbolt &function_symbol, + symbol_tablet &symbol_table) +{ + code_typet &function_type = to_code_type(function_symbol.type); + code_typet::parameterst ¶meters=function_type.parameters(); + for(std::size_t i=0; i #include #include +#include #include "message.h" class symbol_tablet; -class symbolt; class exprt; class namespacet; class typet; @@ -122,7 +122,14 @@ class languaget:public messaget symbolt &symbol, symbol_tablet &symbol_table); + virtual parameter_symbolt build_stub_parameter_symbol( + const symbolt &function_symbol, + size_t parameter_index, + const typet ¶meter_type); private: bool is_symbol_opaque_function(const symbolt &symbol); + void generate_opaque_parameter_symbols( + symbolt &function_symbol, + symbol_tablet &symbol_table); }; #endif // CPROVER_UTIL_LANGUAGE_H From ddd2cae3f66bc1d7b7f417cd0c5690c13bc0ad46 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 2 Dec 2016 12:52:04 +0000 Subject: [PATCH 04/11] Pass the whole parameter in when generating the symbol This allows for the symbol builder to inspect other properties of the type (e.g. is is a this parameter). --- src/util/language.cpp | 4 ++-- src/util/language.h | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/util/language.cpp b/src/util/language.cpp index 7349b09ed1f..b88a7c2f3c7 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -215,7 +215,7 @@ Function: languaget::build_stub_parameter_symbol parameter_symbolt languaget::build_stub_parameter_symbol( const symbolt &function_symbol, size_t parameter_index, - const typet ¶meter_type) + const code_typet::parametert ¶meter) { error() << "language " << id() << " doesn't implement build_stub_parameter_symbol. " @@ -280,7 +280,7 @@ void languaget::generate_opaque_parameter_symbols( { code_typet::parametert ¶m=parameters[i]; const parameter_symbolt ¶m_symbol= - build_stub_parameter_symbol(function_symbol, i, param.type()); + build_stub_parameter_symbol(function_symbol, i, param); param.set_base_name(param_symbol.base_name); param.set_identifier(param_symbol.name); diff --git a/src/util/language.h b/src/util/language.h index 9ec92ebc406..214b9ed2813 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "message.h" @@ -125,7 +126,7 @@ class languaget:public messaget virtual parameter_symbolt build_stub_parameter_symbol( const symbolt &function_symbol, size_t parameter_index, - const typet ¶meter_type); + const code_typet::parametert ¶meter); private: bool is_symbol_opaque_function(const symbolt &symbol); void generate_opaque_parameter_symbols( From b12d2e720015fd5f287843380cf2ce3f53cd513e Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 5 Dec 2016 14:30:57 +0000 Subject: [PATCH 05/11] Refactored method for generating return symbol name to languaget The name for the return symbol is now generated by languaget. This is so the name is consistent across different language implementations. --- src/util/language.cpp | 22 ++++++++++++++++++++++ src/util/language.h | 3 +++ 2 files changed, 25 insertions(+) diff --git a/src/util/language.cpp b/src/util/language.cpp index b88a7c2f3c7..d395d063903 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -224,6 +224,28 @@ parameter_symbolt languaget::build_stub_parameter_symbol( return parameter_symbolt(); } +/*******************************************************************\ + +Function: languaget::get_stub_return_symbol_name + + Inputs: + function_id - the function that has a return value + + Outputs: the identifier to use for the symbol that will store the + return value of this function. + + Purpose: To get the name of the symbol to be used for the return value + of the function. Generates a name like to_return_function_name + +\*******************************************************************/ + +irep_idt languaget::get_stub_return_symbol_name(const irep_idt &function_id) +{ + std::ostringstream return_symbol_name_builder; + return_symbol_name_builder << "to_return_" << function_id; + return return_symbol_name_builder.str(); +} + /*******************************************************************\ diff --git a/src/util/language.h b/src/util/language.h index 214b9ed2813..d78477e8ab4 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -127,6 +127,9 @@ class languaget:public messaget const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert ¶meter); + + static irep_idt get_stub_return_symbol_name(const irep_idt &function_id); + private: bool is_symbol_opaque_function(const symbolt &symbol); void generate_opaque_parameter_symbols( From 13038bf325dd021fb029de9ec99dda4040174ad4 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 17 Jan 2017 12:43:22 +0000 Subject: [PATCH 06/11] Added a flag for enabling opaque method stubs As some tests were verifying the functions didn't exist, we need a flag to turn it on or off. Stubs default to off and are turned on by the flag --generate-opaque-stubs. This is an option in CBMC but perhaps it could be applied to other programs (e.g. applied when compiling C to GOTO). --- src/langapi/language_ui.cpp | 4 ++++ src/util/language.cpp | 44 +++++++++++++++++++++++++++---------- src/util/language.h | 4 ++++ src/util/language_file.cpp | 22 +++++++++++++++++++ src/util/language_file.h | 2 ++ 5 files changed, 65 insertions(+), 11 deletions(-) diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 95b5d104a4f..4b0f3fa0d75 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -183,6 +183,10 @@ bool language_uit::final() { language_files.set_message_handler(*message_handler); + // Enable/disable stub generation for opaque methods + bool stubs_enabled=_cmdline.isset("generate-opaque-stubs"); + language_files.set_should_generate_opaque_method_stubs(stubs_enabled); + if(language_files.final(symbol_table)) { if(get_ui()==ui_message_handlert::PLAIN) diff --git a/src/util/language.cpp b/src/util/language.cpp index d395d063903..2b546f365a5 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -133,6 +133,24 @@ bool languaget::type_to_name( /*******************************************************************\ +Function: languaget::set_should_generate_opaque_method_stubs + + Inputs: + should_generate_stubs - Should stub generation be enabled + + Outputs: + + Purpose: Turn on or off stub generation. + +\*******************************************************************/ +void languaget::set_should_generate_opaque_method_stubs( + bool should_generate_stubs) +{ + generate_opaque_stubs=should_generate_stubs; +} + +/*******************************************************************\ + Function: languaget::generate_opaque_method_stubs Inputs: @@ -143,27 +161,31 @@ Function: languaget::generate_opaque_method_stubs Purpose: When there are opaque methods (e.g. ones where we don't have a body), we create a stub function in the goto program and mark it as opaque so the interpreter fills in - appropriate values for it. + appropriate values for it. This will only happen if + generate_opaque_stubs is enabled. \*******************************************************************/ void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) { - for(auto &symbol_entry : symbol_table.symbols) + if(generate_opaque_stubs) { - if(is_symbol_opaque_function(symbol_entry.second)) + for(auto &symbol_entry : symbol_table.symbols) { - symbolt &symbol=symbol_entry.second; + if(is_symbol_opaque_function(symbol_entry.second)) + { + symbolt &symbol=symbol_entry.second; - generate_opaque_parameter_symbols(symbol, symbol_table); + generate_opaque_parameter_symbols(symbol, symbol_table); - irep_idt return_symbol_id = generate_opaque_stub_body( - symbol, - symbol_table); + irep_idt return_symbol_id=generate_opaque_stub_body( + symbol, + symbol_table); - if(return_symbol_id!=ID_nil) - { - symbol.type.set("opaque_method_capture_symbol", return_symbol_id); + if(return_symbol_id!=ID_nil) + { + symbol.type.set("opaque_method_capture_symbol", return_symbol_id); + } } } } diff --git a/src/util/language.h b/src/util/language.h index d78477e8ab4..b83bba97c0b 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -112,6 +112,8 @@ class languaget:public messaget virtual languaget *new_language()=0; + void set_should_generate_opaque_method_stubs(bool should_generate_stubs); + // constructor / destructor languaget() { } @@ -130,6 +132,8 @@ class languaget:public messaget static irep_idt get_stub_return_symbol_name(const irep_idt &function_id); + bool generate_opaque_stubs; + private: bool is_symbol_opaque_function(const symbolt &symbol); void generate_opaque_parameter_symbols( diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp index 46f51564b54..b0fbb47c2f9 100644 --- a/src/util/language_file.cpp +++ b/src/util/language_file.cpp @@ -93,6 +93,28 @@ void language_filest::show_parse(std::ostream &out) /*******************************************************************\ +Function: language_filest::set_should_generate_opqaue_method_stubs + + Inputs: + should_generate_stubs - Should stub generation be enabled + + Outputs: + + Purpose: Turn on or off stub generation for all the languages + +\*******************************************************************/ + +void language_filest::set_should_generate_opaque_method_stubs( + bool stubs_enabled) +{ + for(file_mapt::value_type &language_file_entry : file_map) + { + languaget *language=language_file_entry.second.language; + language->set_should_generate_opaque_method_stubs(stubs_enabled); + } +} + +/*******************************************************************\ Function: language_filest::parse Inputs: diff --git a/src/util/language_file.h b/src/util/language_file.h index d3184d48697..9fffc7f14f1 100644 --- a/src/util/language_file.h +++ b/src/util/language_file.h @@ -75,6 +75,8 @@ class language_filest:public messaget file_map.clear(); } + void set_should_generate_opaque_method_stubs(bool stubs_enabled); + bool parse(); void show_parse(std::ostream &out); From f9bfbbebbdb65bf113338c96647ef20b4e5a7977 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 16 Jan 2017 17:03:48 +0000 Subject: [PATCH 07/11] Use the system_library_symbols when generating stubs We don't want to generate stubs for any of these symbols as they have proper internal implementaions that CBMC knows about. --- src/util/language.cpp | 9 +++++---- src/util/language.h | 3 +++ 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/util/language.cpp b/src/util/language.cpp index 2b546f365a5..5a5eb2417ea 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -170,6 +170,8 @@ void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) { if(generate_opaque_stubs) { + system_symbols=system_library_symbolst(); + for(auto &symbol_entry : symbol_table.symbols) { if(is_symbol_opaque_function(symbol_entry.second)) @@ -287,14 +289,13 @@ Function: languaget::is_symbol_opaque_function bool languaget::is_symbol_opaque_function(const symbolt &symbol) { - // Explictly exclude CPROVER functions since these aren't opaque - std::string variable_id_str(symbol.name.c_str()); - bool is_cprover_function = has_prefix(variable_id_str, CPROVER_PREFIX); + std::set headers; + bool is_internal=system_symbols.is_symbol_internal_symbol(symbol, headers); return !symbol.is_type && symbol.value.id()==ID_nil && symbol.type.id()==ID_code && - !is_cprover_function; + !is_internal; } /*******************************************************************\ diff --git a/src/util/language.h b/src/util/language.h index b83bba97c0b..73ead1cd8e4 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "message.h" @@ -139,5 +140,7 @@ class languaget:public messaget void generate_opaque_parameter_symbols( symbolt &function_symbol, symbol_tablet &symbol_table); + + system_library_symbolst system_symbols; }; #endif // CPROVER_UTIL_LANGUAGE_H From 473dc8970e3d08689f0bc224a4a3d049bfe3a854 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 19 Jan 2017 10:54:04 +0000 Subject: [PATCH 08/11] Added comment explaining the type of symbols we aren't stubbing --- src/util/language.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/util/language.cpp b/src/util/language.cpp index 5a5eb2417ea..ddb41979040 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -290,6 +290,9 @@ Function: languaget::is_symbol_opaque_function bool languaget::is_symbol_opaque_function(const symbolt &symbol) { std::set headers; + // Don't create stubs for symbols like: + // __CPROVER_blah (which aren't real external functions) + // and strstr (which we will model for ourselves later) bool is_internal=system_symbols.is_symbol_internal_symbol(symbol, headers); return !symbol.is_type && From 519e08bf9591e9b3db31f8bffcd34862d6e93151 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 8 Nov 2016 17:03:58 +0000 Subject: [PATCH 09/11] Adding simple regression for struct function Also made test logs be ignored but git. This test currently fails (correctly) as the integer member of the struct is not being set to the correct value --- regression/.gitignore | 1 + 1 file changed, 1 insertion(+) create mode 100644 regression/.gitignore diff --git a/regression/.gitignore b/regression/.gitignore new file mode 100644 index 00000000000..750ecf9f446 --- /dev/null +++ b/regression/.gitignore @@ -0,0 +1 @@ +tests.log From 0e755e61aa3a7c0c0eb6577b896c8e9fdeca61fb Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 9 Dec 2016 16:42:13 +0000 Subject: [PATCH 10/11] Use the symbol in expr2c --- src/ansi-c/expr2c.cpp | 46 +++++++++++++++++++++++++++---------------- 1 file changed, 29 insertions(+), 17 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a6975bdab19..5de8c7688b0 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -518,28 +518,40 @@ std::string expr2ct::convert_rec( } else if(src.id()==ID_symbol) { - const typet &followed=ns.follow(src); + symbol_typet symbolic_type=to_symbol_type(src); + const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef); - if(followed.id()==ID_struct) + // Providing we have a valid identifer, we can just use that rather than + // trying to find the concrete type + if(typedef_identifer!="") { - std::string dest=q+"struct"; - const irep_idt &tag=to_struct_type(followed).get_tag(); - if(tag!="") - dest+=" "+id2string(tag); - dest+=d; - return dest; + return q+id2string(typedef_identifer)+d; } - else if(followed.id()==ID_union) + else { - std::string dest=q+"union"; - const irep_idt &tag=to_union_type(followed).get_tag(); - if(tag!="") - dest+=" "+id2string(tag); - dest+=d; - return dest; + const typet &followed=ns.follow(src); + + if(followed.id()==ID_struct) + { + std::string dest=q+"struct"; + const irep_idt &tag=to_struct_type(followed).get_tag(); + if(tag!="") + dest+=" "+id2string(tag); + dest+=d; + return dest; + } + else if(followed.id()==ID_union) + { + std::string dest=q+"union"; + const irep_idt &tag=to_union_type(followed).get_tag(); + if(tag!="") + dest+=" "+id2string(tag); + dest+=d; + return dest; + } + else + return convert_rec(followed, new_qualifiers, declarator); } - else - return convert_rec(followed, new_qualifiers, declarator); } else if(src.id()==ID_struct_tag) { From 8f68c25654962d3693cdc9e04665c47780421e17 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 10 Mar 2017 11:28:43 +0000 Subject: [PATCH 11/11] Call the generate_opqaue_stubs from final This doesn't do anything if it is not enabled --- src/ansi-c/ansi_c_language.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index dc69515ede2..159b0d6df40 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -196,6 +196,8 @@ Function: ansi_c_languaget::final bool ansi_c_languaget::final(symbol_tablet &symbol_table) { + generate_opaque_method_stubs(symbol_table); + if(ansi_c_entry_point(symbol_table, "main", get_message_handler())) return true;