Use autotune.activated termination as separate switch whether termina…

…tion analysis should be activated (instead of using specification).
goblint · Nov 19, 2023 · 9d8629d · 9d8629d
1 parent 0652213
commit 9d8629d
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -72,8 +72,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
-        "termination",
-        "specification"
+        "termination"
       ]
     }
   },

diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -506,6 +506,9 @@ let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Spe
 let specificationIsActivated () =
   isActivated "specification" && get_string "ana.specification" <> ""
 
+let specificationTerminationIsActivated () =
+  isActivated "termination"
+
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in

diff --git a/src/goblint.ml b/src/goblint.ml
@@ -39,7 +39,7 @@ let main () =
       print_endline GobSys.command_line;
     );
     (* When analyzing a termination specification, activate the termination analysis before pre-processing. *)
-    if get_bool "ana.autotune.enabled" && AutoTune.specificationIsActivated () then AutoTune.focusOnTermination ();
+    if get_bool "ana.autotune.enabled" && AutoTune.specificationTerminationIsActivated () then AutoTune.focusOnTermination ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =