Merge pull request #1234 from goblint/path_sens_memleak

Experiment with path- and context-sensitivity for memLeak analysis
goblint · Nov 9, 2023 · 03e17b6 · 03e17b6
2 parents d47e429 + 90e8b31
commit 03e17b6
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
@@ -96,4 +96,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git 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

diff --git 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",
-Original file line number
+Diff line change
@@ Expand Up / @@ -96,4 +96,4 @@ struct @@
     end
     let _ =
-      MCP.register_analysis (module Spec : MCPSpec)
+      MCP.register_analysis (module Spec : MCPSpec)