Remove dbg.verbose option

conf/incremental.json

@@ -24,7 +24,7 @@
     "earlyglobs": true
   },
   "dbg": {
-    "verbose": true,
+    "level": "debug",
     "trace": {
       "context": true
     },

conf/minimal_incremental.json

@@ -23,7 +23,7 @@
     "earlyglobs": true
   },
   "dbg": {
-    "verbose": true,
+    "level": "debug",
     "trace": {
       "context": true
     },

src/incremental/serialize.ml

@@ -27,7 +27,7 @@ let marshal obj fileName  =
   close_out chan
 
 let unmarshal fileName =
-  if GobConfig.get_bool "dbg.verbose" then
+  if Logs.Level.should_log Debug then
     (* Do NOT replace with Printf because of GobView: https://github.com/goblint/gobview/issues/10 *)
     print_endline ("Unmarshalling " ^ Fpath.to_string fileName ^ "... If type of content changed, this will result in a segmentation fault!");
   Marshal.input (open_in_bin (Fpath.to_string fileName))

src/maingoblint.ml

@@ -14,7 +14,7 @@ let print_version ch =
   printf "Dune profile:    %s\n" ConfigProfile.profile; (* nosemgrep: print-not-logging *)
   printf "OCaml version:   %s\n" Sys.ocaml_version; (* nosemgrep: print-not-logging *)
   printf "OCaml flambda:   %s\n" ConfigOcaml.flambda; (* nosemgrep: print-not-logging *)
-  if get_bool "dbg.verbose" then (
+  if Logs.Level.should_log Debug then (
     printf "Library versions:\n"; (* nosemgrep: print-not-logging *)
     List.iter (fun (name, version) ->
         let version = Option.default "[unknown]" version in
@@ -98,7 +98,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
     complete_option_value !last_complete_option s
   in
   [ "-o"                   , Arg_complete.String (set_string "outfile", Arg_complete.empty), ""
-  ; "-v"                   , Arg_complete.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "dbg.timing.enabled" true), ""
+  ; "-v"                   , Arg_complete.Unit (fun () -> set_string "dbg.level" "debug"; set_bool "dbg.timing.enabled" true), ""
   ; "-j"                   , Arg_complete.Int (set_int "jobs", Arg_complete.empty), ""
   ; "-I"                   , Arg_complete.String (set_string "pre.includes[+]", Arg_complete.empty), ""
   ; "-IK"                  , Arg_complete.String (set_string "pre.kernel_includes[+]", Arg_complete.empty), ""
@@ -164,7 +164,7 @@ let check_arguments () =
 
 (** Initialize some globals in other modules. *)
 let handle_flags () =
-  if get_bool "dbg.verbose" then (
+  if Logs.Level.should_log Debug then (
     Printexc.record_backtrace true;
     Errormsg.debugFlag := true;
     Errormsg.verboseFlag := true

src/solvers/generic.ml

@@ -12,7 +12,7 @@ module LoadRunSolver: GenericEqSolver =
       let solver_file = "solver.marshalled" in
       let load_run = Fpath.v (get_string "load_run") in
       let solver = Fpath.(load_run / solver_file) in
-      if get_bool "dbg.verbose" then
+      if Logs.Level.should_log Debug then
         (* Do NOT replace with Printf because of GobView: https://github.com/goblint/gobview/issues/10 *)
         print_endline ("Loading the solver result of a saved run from " ^ (Fpath.to_string solver));
       let vh: S.d VH.t = Serialize.unmarshal solver in

src/solvers/td3.ml

@@ -81,21 +81,21 @@ module Base =
     }
 
     let print_data data =
-      Logs.info "|rho|=%d" (HM.length data.rho);
-      Logs.info "|stable|=%d" (HM.length data.stable);
-      Logs.info "|infl|=%d" (HM.length data.infl);
-      Logs.info "|wpoint|=%d" (HM.length data.wpoint);
-      Logs.info "|sides|=%d" (HM.length data.sides);
-      Logs.info "|side_dep|=%d" (HM.length data.side_dep);
-      Logs.info "|side_infl|=%d" (HM.length data.side_infl);
-      Logs.info "|var_messages|=%d" (HM.length data.var_messages);
-      Logs.info "|rho_write|=%d" (HM.length data.rho_write);
-      Logs.info "|dep|=%d" (HM.length data.dep);
+      Logs.debug "|rho|=%d" (HM.length data.rho);
+      Logs.debug "|stable|=%d" (HM.length data.stable);
+      Logs.debug "|infl|=%d" (HM.length data.infl);
+      Logs.debug "|wpoint|=%d" (HM.length data.wpoint);
+      Logs.debug "|sides|=%d" (HM.length data.sides);
+      Logs.debug "|side_dep|=%d" (HM.length data.side_dep);
+      Logs.debug "|side_infl|=%d" (HM.length data.side_infl);
+      Logs.debug "|var_messages|=%d" (HM.length data.var_messages);
+      Logs.debug "|rho_write|=%d" (HM.length data.rho_write);
+      Logs.debug "|dep|=%d" (HM.length data.dep);
       Hooks.print_data ()
 
     let print_data_verbose data str =
-      if GobConfig.get_bool "dbg.verbose" then (
-        Logs.info "%s:" str;
+      if Logs.Level.should_log Debug then (
+        Logs.debug "%s:" str;
         print_data data
       )
 
@@ -781,7 +781,7 @@ module Base =
         incr i;
         let unstable_vs = List.filter (neg (HM.mem stable)) vs in
         if unstable_vs <> [] then (
-          if GobConfig.get_bool "dbg.verbose" then (
+          if Logs.Level.should_log Debug then (
             if !i = 1 then Logs.newline ();
             Logs.debug "Unstable solver start vars in %d. phase:" !i;
             List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs;
@@ -1095,7 +1095,7 @@ module DepVals: GenericEqIncrSolver =
       module HM = HM
 
       let print_data () =
-        Logs.info "|dep_vals|=%d" (HM.length !current_dep_vals)
+        Logs.debug "|dep_vals|=%d" (HM.length !current_dep_vals)
 
       let system x =
         match S.system x with

src/transform/expressionEvaluation.ml

@@ -37,9 +37,6 @@ struct
     | Some value -> value
     | None -> raise Stdlib.Exit
 
-  let is_debug () =
-    GobConfig.get_bool "dbg.verbose"
-
   let string_of_evaluation_result evaluation_result =
     match evaluation_result with
     | Some value -> if value then "TRUE" else "FALSE"
@@ -84,15 +81,15 @@ struct
         match ~? (fun () -> Formatcil.cExp expression_string (local_variables @ global_variables)) with
         (* Expression unparseable at this location *)
         | None ->
-          if is_debug () then Logs.debug "| (Unparseable)";
+          Logs.debug "| (Unparseable)";
           Some false
         (* Successfully parsed expression *)
         | Some expression ->
           (* Evaluate at (directly before) the location *)
           match self#try_ask location expression with
           (* Dead code or not listed as part of the control flow *)
           | None ->
-            if is_debug () then Logs.debug "| (Unreachable)";
+            Logs.debug "| (Unreachable)";
             Some false
           (* Valid location *)
           | Some value_before ->
@@ -116,17 +113,11 @@ struct
               (* Prefer successor evaluation *)
               match successor_evaluation with
               | None ->
-                if is_debug () then
-                  begin
-                    Logs.debug "%s" ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement))
-                  end;
+                Logs.debug "%s" ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement));
                 value_before
               | Some value_after ->
-                if is_debug () then
-                  begin
-                    Logs.debug "%s" ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/");
-                    Logs.debug "%s" ("| " ^ (~! !succeeding_statement |> string_of_statement))
-                  end;
+                Logs.debug "%s" ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/");
+                Logs.debug "%s" ("| " ^ (~! !succeeding_statement |> string_of_statement));
                 value_after
 
       method private try_ask location expression =
@@ -155,8 +146,7 @@ struct
       | Error message ->
         Error ("ExpEval: Unable to parse JSON query file: \"" ^ name ^ "\" (" ^ message ^ ")")
       | Ok query ->
-        if is_debug () then
-          Logs.debug "Successfully parsed JSON query file: \"%s\"" name;
+        Logs.debug "Successfully parsed JSON query file: \"%s\"" name;
         Ok query
 
   let string_of_location (location : Cil.location) =
@@ -199,11 +189,13 @@ struct
         | Some value ->
           if value then
             Logs.info "%s" (loc |> string_of_location)
-          else if is_debug () then
+          else
             Logs.debug "%s x" (loc |> string_of_location)
         | None ->
-          if query.mode = `May || is_debug () then
+          if query.mode = `May then
             Logs.info "%s ?" (loc |> string_of_location)
+          else
+            Logs.debug "%s ?" (loc |> string_of_location)
       in
       gv_results := results;
       List.iter print results

src/util/options.schema.json

@@ -1775,12 +1775,6 @@
           "enum": ["debug", "info", "warning", "error"],
           "default": "info"
         },
-        "verbose": {
-          "title": "dbg.verbose",
-          "description": "Prints some status information.",
-          "type": "boolean",
-          "default": false
-        },
         "timing": {
           "title": "dbg.timing",
           "type": "object",

tests/regression/68-longjmp/42-poison-reduced.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --enable dbg.verbose --disable exp.volatiles_are_top --enable ana.int.interval
+// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --disable exp.volatiles_are_top --enable ana.int.interval
 #include<setjmp.h>
 jmp_buf env_buffer;
 struct c {

tests/regression/68-longjmp/47-more-reduced.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --enable dbg.verbose --disable exp.volatiles_are_top --enable ana.int.interval
+// PARAM: --set ana.activated[+] expsplit --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.invalidate.args --disable exp.volatiles_are_top --enable ana.int.interval
 #include<setjmp.h>
 jmp_buf env_buffer;