Invoke functions marked __attribute__((destructor))

This is a GCC extension that our front-end parses, but an implementation
of the desired semantics was hitherto missing.

Co-authored-by: Chris Ryder <[email protected]>

Author: tautschnig

regression/cbmc/destructor1/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+#ifdef __GNUC__
+// Will be implicitly invoked after main() completes if the attribute is
+// properly supported
+static __attribute__((destructor)) void assert_false(void)
+{
+  assert(0);
+}
+#endif
+
+int main()
+{
+#ifndef __GNUC__
+  // explicitly invoke assert_false as __attribute__((destructor)) isn't
+  // supported in non-GCC modes
+  assert_false();
+#endif
+}

regression/cbmc/destructor1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^\[assert_false.assertion.1\] line 8 assertion 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/ansi_c_entry_point.cpp

@@ -504,6 +504,26 @@ bool generate_ansi_c_start_function(
 
   record_function_outputs(symbol, init_code, symbol_table);
 
+  // now call destructor functions (a GCC extension)
+
+  for(const auto &symbol_table_entry : symbol_table.symbols)
+  {
+    const symbolt &symbol = symbol_table_entry.second;
+
+    if(symbol.type.id() != ID_code)
+      continue;
+
+    const code_typet &code_type = to_code_type(symbol.type);
+    if(
+      code_type.return_type().id() == ID_destructor &&
+      code_type.parameters().empty())
+    {
+      code_function_callt destructor_call(symbol.symbol_expr());
+      destructor_call.add_source_location() = symbol.location;
+      init_code.add(std::move(destructor_call));
+    }
+  }
+
   // add the entry point symbol
   symbolt new_symbol;