Merge pull request #1682 from goblint/memleak-assert

Ensure that `__goblint_check` does not affect memLeak analysis

Author: sim642

src/analyses/memLeak.ml

@@ -227,7 +227,7 @@ struct
       (* Upon a call to the "Abort" special function in the multi-threaded case, we give up and conservatively warn *)
       warn_for_multi_threaded_due_to_abort man;
       state
-    | Assert { exp; _ } ->
+    | Assert { exp; refine = true; _ } ->
       begin match man.ask (Queries.EvalInt exp) with
         | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
         | a ->

tests/regression/76-memleak/32-no-mem-leak-goblint-check.c

@@ -0,0 +1,9 @@
+// PARAM: --set ana.activated[+] memLeak --set ana.malloc.unique_address_count 1
+#include <stdlib.h>
+#include <goblint.h>
+
+int main() {
+    int *ptr = malloc(sizeof(int));
+    __goblint_check(ptr == 0); // FAIL
+    free(ptr);
+}

tests/regression/76-memleak/32-no-mem-leak-goblint-check.t

@@ -0,0 +1,6 @@
+  $ goblint --set ana.activated[+] memLeak --set ana.malloc.unique_address_count 1 32-no-mem-leak-goblint-check.c
+  [Error][Assert] Assertion "(unsigned long )ptr == (unsigned long )((int *)0)" will fail. (32-no-mem-leak-goblint-check.c:7:5-7:30)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 5
+    dead: 0
+    total lines: 5

tests/regression/76-memleak/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))