From 1cf3942190226126befdac561159c15758153a52 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 31 Oct 2023 16:07:47 +0200 Subject: [PATCH] Make memsafety autotuner enable ana.arrayoob (PR #1201) https://github.com/goblint/analyzer/pull/1201#issuecomment-1787126733 --- src/autoTune.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/autoTune.ml b/src/autoTune.ml index 186d930189..b96848c841 100644 --- 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 (