Linking library functions: support constructor functions

With 7f1cc0f we may remove `__CPROVER_initialize` from the goto
model, which in turn made us fail to consider constructors called from
it among the set of called functions (as well as any functions
(transitively) called from these).

Author: tautschnig

regression/cbmc/constructor2/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#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;
+}

regression/cbmc/constructor2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+map::at
+^warning: ignoring

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;

src/goto-programs/link_to_library.cpp

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "link_goto_model.h"
 
 /// Try to add \p missing_function from \p library to \p goto_model.
-static optionalt<replace_symbolt::expr_mapt> add_one_function(
+static std::pair<optionalt<replace_symbolt::expr_mapt>, bool> add_one_function(
   goto_modelt &goto_model,
   message_handlert &message_handler,
   const std::function<void(
@@ -49,6 +49,7 @@ static optionalt<replace_symbolt::expr_mapt> 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<replace_symbolt::expr_mapt> 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);