diff --git a/src/autoTune.ml b/src/autoTune.ml index cc1af59940..4b959749a7 100644 --- 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 index 4ea3a3d242..6c5a2df33d 100644 --- 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 =