diff --git a/regression/cbmc/constructor2/main.c b/regression/cbmc/constructor2/main.c new file mode 100644 index 00000000000..03f7d1b8fb9 --- /dev/null +++ b/regression/cbmc/constructor2/main.c @@ -0,0 +1,21 @@ +#include +#include + +#ifdef __GNUC__ +int x; + +__attribute__((constructor)) void init_heap() +{ + int *p = malloc(sizeof(int)); + free(p); + x = 42; +} +#endif + +int main() +{ +#ifdef __GNUC__ + assert(x == 42); +#endif + return 0; +} diff --git a/regression/cbmc/constructor2/test.desc b/regression/cbmc/constructor2/test.desc new file mode 100644 index 00000000000..da96dcddeee --- /dev/null +++ b/regression/cbmc/constructor2/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +map::at +^warning: ignoring diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 327ae44593a..b836600bd82 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -271,6 +271,7 @@ __CPROVER_HIDE:; #undef free +void __CPROVER_deallocate(void *); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); #ifndef LIBRARY_CHECK const void *__CPROVER_alloca_object = 0; diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 2e656cf589f..b2b5bb00c15 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "link_goto_model.h" /// Try to add \p missing_function from \p library to \p goto_model. -static optionalt add_one_function( +static std::pair, bool> add_one_function( goto_modelt &goto_model, message_handlert &message_handler, const std::function add_one_function( } // check whether additional initialization may be required + bool init_required = false; if( goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) != goto_model.goto_functions.function_map.end()) @@ -60,13 +61,15 @@ static optionalt add_one_function( !entry.second.is_macro && entry.second.type.id() != ID_code && !goto_model.symbol_table.has_symbol(entry.first)) { - goto_model.unload(INITIALIZE_FUNCTION); + init_required = true; break; } } } - return link_goto_model(goto_model, std::move(library_model), message_handler); + return { + link_goto_model(goto_model, std::move(library_model), message_handler), + init_required}; } /// Complete missing function definitions using the \p library. @@ -95,9 +98,7 @@ void link_to_library( // forward declarations, or perhaps even cases of missing forward // declarations) may result in type changes to objects. replace_symbolt::expr_mapt object_type_updates; - const bool had_init = - goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) != - goto_model.goto_functions.function_map.end(); + bool need_reinit = false; while(true) { @@ -125,8 +126,10 @@ void link_to_library( changed = true; added_functions.insert(id); - auto updates_opt = + auto one_result = add_one_function(goto_model, message_handler, library, id); + auto updates_opt = one_result.first; + need_reinit |= one_result.second; if(!updates_opt.has_value()) { messaget log{message_handler}; @@ -143,11 +146,9 @@ void link_to_library( break; } - if( - had_init && - goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) == - goto_model.goto_functions.function_map.end()) + if(need_reinit) { + goto_model.unload(INITIALIZE_FUNCTION); static_lifetime_init( goto_model.symbol_table, goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location);