Replace merged direct printing with Logs

goblint · Jan 10, 2024 · a354ce3 · a354ce3
1 parent eb8b14d
commit a354ce3
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -216,23 +216,23 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
   match spec with
   | ValidFree -> (* Enable the useAfterFree analysis *)
     let uafAna = ["useAfterFree"] in
-    print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
+    Logs.info "Specification: ValidFree -> enabling useAfterFree analysis \"%s\"" (String.concat ", " uafAna);
     enableAnalyses uafAna
   | ValidDeref -> (* Enable the memOutOfBounds analysis *)
     let memOobAna = ["memOutOfBounds"] in
     set_bool "ana.arrayoob" true;
-    print_endline "Setting \"cil.addNestedScopeAttr\" to true";
+    Logs.info "Setting \"cil.addNestedScopeAttr\" to true";
     set_bool "cil.addNestedScopeAttr" true;
-    print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
+    Logs.info "Specification: ValidDeref -> enabling memOutOfBounds analysis \"%s\"" (String.concat ", " memOobAna);
     enableAnalyses memOobAna;
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in
     if (get_int "ana.malloc.unique_address_count") < 1 then (
-      print_endline "Setting \"ana.malloc.unique_address_count\" to 5";
+      Logs.info "Setting \"ana.malloc.unique_address_count\" to 5";
       set_int "ana.malloc.unique_address_count" 5;
     );
-    print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
+    Logs.info "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"%s\"" (String.concat ", " memLeakAna);
     enableAnalyses memLeakAna
   | _ -> ()
 
@@ -243,7 +243,7 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
   match spec with
   | Termination ->
     let terminationAnas = ["termination"; "threadflag"; "apron"] in
-    print_endline @@ "Specification: Termination -> enabling termination analyses \"" ^ (String.concat ", " terminationAnas) ^ "\"";
+    Logs.info "Specification: Termination -> enabling termination analyses \"%s\"" (String.concat ", " terminationAnas);
     enableAnalyses terminationAnas;
     set_string "sem.int.signed_overflow" "assume_none";
     set_bool "ana.int.interval" true;
@@ -482,7 +482,7 @@ let activateTmpSpecialAnalysis () =
   in
   let hasMathFunctions = hasFunction isMathFun in
   if hasMathFunctions then (
-    print_endline @@ "math function -> enabling tmpSpecial analysis and floating-point domain";
+    Logs.info "math function -> enabling tmpSpecial analysis and floating-point domain";
     enableAnalyses ["tmpSpecial"];
     set_bool "ana.float.interval" true;
   )

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
@@ -449,7 +449,7 @@ class loopUnrollingVisitor(func, totalLoops) = object
       let duplicate_and_rem_labels s =
         let factor = loop_unrolling_factor s func totalLoops in
         if(factor > 0) then (
-          print_endline @@ "unrolling loop at " ^ CilType.Location.show loc ^" with factor " ^ string_of_int factor;
+          Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor;
           annotateArrays b;
           match s.skind with
           | Loop (b,loc, loc2, break , continue) ->