Call Autotune.focusOnSpecification before preprocessing, as terminati…

…no analysis needs to be activated before preprocessing to work.
goblint · Nov 17, 2023 · a4adabd · a4adabd
1 parent 28dca49
commit a4adabd
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -496,6 +496,9 @@ let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_
 
 let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ())
 
+let specificationIsActivated () =
+  isActivated "specification" && get_string "ana.specification" <> ""
+
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in
@@ -515,8 +518,8 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if isActivated "specification" && get_string "ana.specification" <> "" then
-    focusOnSpecification ();
+  (* if specificationIsActivated () then
+     focusOnSpecification (); *)
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;

diff --git a/src/goblint.ml b/src/goblint.ml
@@ -38,6 +38,8 @@ let main () =
       print_endline (GobUnix.localtime ());
       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.focusOnSpecification ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =