Fix memory leak check for __VERIFIER_error

peterschrammel · peterschrammel · commit 507d221ff43e · 2018-11-25T20:16:12.000+05:30
diff --git a/regression/cbmc/Memory_leak_abort/main.c b/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;
 }
diff --git a/regression/cbmc/Memory_leak_abort/test.desc b/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
diff --git a/src/analyses/goto_check.cpp b/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);
       }
diff --git a/src/goto-programs/builtin_functions.cpp b/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);
   }

Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`#include <stdlib.h>`
`2`	`2`
`3`		`-extern void __VERIFIER_error() __attribute__ ((__noreturn__));`
	`3`	`+extern void __VERIFIER_error() __attribute__((__noreturn__));`
`4`	`4`
`5`	`5`	`int main()`
`6`	`6`	`{`
`@@ -11,6 +11,8 @@ int main()`
`11`	`11`	`exit(1);`
`12`	`12`	`if(*p == 2)`
`13`	`13`	`_Exit(1);`
	`14`	`+ if(*p == 3)`
	`15`	`+ __VERIFIER_error();`
`14`	`16`	`free(p);`
`15`	`17`	`return 0;`
`16`	`18`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1708,7 +1708,8 @@ void goto_checkt::goto_check(`
`1708`	`1708`	`if(`
`1709`	`1709`	`enable_memory_leak_check && simplified_guard.is_false() &&`
`1710`	`1710`	`(i.function == "abort" \|\| i.function == "exit" \|\|`
`1711`		`- i.function == "_Exit"))`
	`1711`	`+ i.function == "_Exit" \|\|`
	`1712`	`+ (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))`
`1712`	`1713`	`{`
`1713`	`1714`	`memory_leak_check(i.function);`
`1714`	`1715`	`}`
Original file line number	Diff line number	Diff line change
`@@ -711,6 +711,7 @@ void goto_convertt::do_function_call_symbol(`
`711`	`711`	`// are being checked`
`712`	`712`	`goto_programt::targett a=dest.add_instruction(ASSUME);`
`713`	`713`	`a->guard=false_exprt();`
	`714`	`+ a->labels.push_back("__VERIFIER_abort");`
`714`	`715`	`a->source_location=function.source_location();`
`715`	`716`	`a->source_location.set("user-provided", true);`
`716`	`717`	`}`