Separate memsafetySpecification autotuner and enable in svcomp conf

Normal specification autotuner does other things we didn't want in SV-COMP.
goblint · Oct 31, 2023 · 6131273 · 6131273
1 parent 1cf3942
commit 6131273
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -70,7 +70,8 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic"
+        "loopUnrollHeuristic",
+        "memsafetySpecification"
       ]
     }
   },

diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
@@ -544,7 +544,7 @@
               "type": "array",
               "items": { "type": "string" },
               "default": [
-                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds"
+                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification"
               ]
             }
           },

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
@@ -186,7 +186,7 @@ let handle_options () =
   check_arguments ();
   AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
-  if AutoTune.isActivated "specification" && get_string "ana.specification" <> "" then
+  if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then
     AutoTune.focusOnMemSafetySpecification ();
   Cilfacade.init_options ();
   handle_flags ()