Make memsafety autotuner enable ana.arrayoob (PR #1201)

#1201 (comment)
goblint · Oct 31, 2023 · 1cf3942 · 1cf3942
1 parent a2a4fa2
commit 1cf3942
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -218,6 +218,7 @@ let focusOnMemSafetySpecification () =
     enableAnalyses uafAna
   | ValidDeref -> (* Enable the memOutOfBounds analysis *)
     let memOobAna = ["memOutOfBounds"] in
+    set_bool "ana.arrayoob" true;
     print_endline "Setting \"cil.addNestedScopeAttr\" to true";
     set_bool "cil.addNestedScopeAttr" true;
     print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
@@ -232,6 +233,7 @@ let focusOnMemSafetySpecification () =
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
+    set_bool "ana.arrayoob" true;
     (print_endline "Setting \"cil.addNestedScopeAttr\" to true";
      set_bool "cil.addNestedScopeAttr" true;
      if (get_int "ana.malloc.unique_address_count") < 1 then (