From 04516adf08e43517eb13bcfcf3fb06dda310c164 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 3 Nov 2023 12:58:46 +0100
Subject: [PATCH 1/2] Make memLeak path- & ctx-sensitive

---
 src/analyses/memLeak.ml             | 7 ++++---
 src/common/util/options.schema.json | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index dbaa2d69fc..62b6bbe3a7 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -14,9 +14,10 @@ struct
   let name () = "memLeak"
 
   module D = ToppedVarInfoSet
-  module C = Lattice.Unit
+  module C = D
+  module P = IdentityP (D)
 
-  let context _ _ = ()
+  let context _ d = d
 
   (* HELPER FUNCTIONS *)
   let warn_for_multi_threaded ctx =
@@ -95,4 +96,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 40669ff729..4e282b19a4 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -352,7 +352,7 @@
           "description": "List of path-sensitive analyses",
           "type": "array",
           "items": { "type": "string" },
-          "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp" ]
+          "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp","memLeak" ]
         },
         "ctx_insens": {
           "title": "ana.ctx_insens",

From 27cf7f58c44e50d45bf5e98ef8ad097d0ed126b9 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 3 Nov 2023 14:05:30 +0100
Subject: [PATCH 2/2] Set unique address count to 5

---
 src/autoTune.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 06347f3190..7ddc1aee43 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -227,8 +227,8 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in
     if (get_int "ana.malloc.unique_address_count") < 1 then (
-      print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
-      set_int "ana.malloc.unique_address_count" 1;
+      print_endline "Setting \"ana.malloc.unique_address_count\" to 5";
+      set_int "ana.malloc.unique_address_count" 5;
     );
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna