Add memory leak instrumentation to abort and exit

Author: peterschrammel

regression/cbmc/Memory_leak_abort/main.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+int main() {
+  int *p = malloc(sizeof(int));
+  if(*p == 0)
+    abort();
+  if(*p == 1)
+    exit(1);
+  if(*p == 2)
+    _Exit(1);
+  free(p);
+  return 0;
+}

regression/cbmc/Memory_leak_abort/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--memory-leak-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+_Exit\.memory-leak\.1.*FAILURE
+__CPROVER__start\.memory-leak\.1.*SUCCESS
+abort\.memory-leak\.1.*FAILURE
+exit\.memory-leak\.1.*FAILURE
+--
+^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -53,6 +53,7 @@ rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
+rm Memory_leak_abort/test.desc
 rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
 rm Multi_Dimensional_Array3/test.desc

src/analyses/goto_check.cpp

@@ -1703,6 +1703,15 @@ void goto_checkt::goto_check(
     }
     else if(i.is_assume())
     {
+      // These are further 'exit points' of the program
+      const exprt simplified_guard = simplify_expr(i.guard, ns);
+      if(
+        enable_memory_leak_check && simplified_guard.is_false() &&
+        (i.function == "abort" || i.function == "exit" ||
+         i.function == "_Exit"))
+      {
+        memory_leak_check(i.function);
+      }
       if(!enable_assumptions)
       {
         i.make_skip();