Fix memory leak check for __VERIFIER_error

Author: peterschrammel

regression/cbmc/Memory_leak_abort/main.c

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

regression/cbmc/Memory_leak_abort/test.desc

@@ -1,12 +1,14 @@
 CORE
 main.c
---memory-leak-check
+--memory-leak-check --no-assertions
 ^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
+main\.memory-leak\.1.*FAILURE
 --
+main\.assertion\.1.*FAILURE
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -1708,7 +1708,8 @@ void goto_checkt::goto_check(
       if(
         enable_memory_leak_check && simplified_guard.is_false() &&
         (i.function == "abort" || i.function == "exit" ||
-         i.function == "_Exit"))
+         i.function == "_Exit" ||
+         (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
       {
         memory_leak_check(i.function);
       }

src/goto-programs/builtin_functions.cpp

@@ -711,6 +711,7 @@ void goto_convertt::do_function_call_symbol(
     // are being checked
     goto_programt::targett a=dest.add_instruction(ASSUME);
     a->guard=false_exprt();
+    a->labels.push_back("__VERIFIER_abort");
     a->source_location=function.source_location();
     a->source_location.set("user-provided", true);
   }