diff --git a/regression/cbmc/destructor1/main.c b/regression/cbmc/destructor1/main.c
new file mode 100644
index 00000000000..07c901db268
--- /dev/null
+++ b/regression/cbmc/destructor1/main.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+
+#ifdef __GNUC__
+// Will be implicitly invoked after main() completes if the attribute is
+// properly supported
+__attribute__((destructor))
+#endif
+void assert_false(void)
+{
+  assert(0);
+}
+
+int main()
+{
+#ifndef __GNUC__
+  // explicitly invoke assert_false as __attribute__((destructor)) isn't
+  // supported in non-GCC modes
+  assert_false();
+#endif
+}
diff --git a/regression/cbmc/destructor1/test.desc b/regression/cbmc/destructor1/test.desc
new file mode 100644
index 00000000000..d386a6e31ac
--- /dev/null
+++ b/regression/cbmc/destructor1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^\[assert_false.assertion.1\] line 10 assertion 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 41f134b6f1b..dcdbe610f2b 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/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;