Remove option dbg.dump

src/common/util/messages.ml

@@ -180,10 +180,6 @@ let () = AfterConfig.register (fun () ->
 (** The file where everything is output *)
 let out = ref stdout
 
-let get_out name alternative = match get_string "dbg.dump" with
-  | "" -> alternative
-  | path -> open_out (Filename.concat path (name ^ ".out"))
-
 
 let print ?(ppf= !formatter) (m: Message.t) =
   let severity_stag = match m.severity with

src/config/options.schema.json

@@ -2128,12 +2128,6 @@
           },
           "additionalProperties": false
         },
-        "dump": {
-          "title": "dbg.dump",
-          "description": "Dumps the results to the given path",
-          "type": "string",
-          "default": ""
-        },
         "cilout": {
           "title": "dbg.cilout",
           "description": "Where to dump cil output",

src/framework/analysisResult.ml

@@ -25,23 +25,16 @@ struct
     )
 end
 
-module type ResultConf =
-sig
-  val result_name: string
-end
-
 module type Result =
 sig
-  include ResultConf
   module Range: Printable.S
   module H: BatHashtbl.S with type key := ResultNode.t
   include BatHashtbl.S with type 'a t := 'a H.t and type key := ResultNode.t
   type t = Range.t H.t
 end
 
-module Result (Range: Printable.S) (C: ResultConf): Result with module Range = Range =
+module Result (Range: Printable.S): Result with module Range = Range =
 struct
-  include C
   module Range = Range
   module H = BatHashtbl.Make (ResultNode)
   include H

src/framework/analysisResultOutput.ml

@@ -42,7 +42,7 @@ struct
 
   let output table live gtable gtfxml (module FileCfg: MyCFG.FileCfg) =
     let file = FileCfg.file in
-    let out = Messages.get_out result_name !Messages.out in
+    let out = !Messages.out in
     match get_string "result" with
     | "pretty" -> ignore (fprintf out "%a\n" pretty (Lazy.force table))
     | "pretty-deterministic" -> ignore (fprintf out "%a\n" pretty_deterministic (Lazy.force table))

src/framework/control.ml

@@ -102,7 +102,7 @@ struct
   (* Set of triples [RT] *)
   module LT = SetDomain.HeadlessSet (RT)
   (* Analysis result structure---a hashtable from program points to [LT] *)
-  module Result = AnalysisResult.Result (LT) (struct let result_name = "analysis" end)
+  module Result = AnalysisResult.Result (LT)
   module ResultOutput = AnalysisResultOutput.Make (Result)
 
   module Query = ResultQuery.Query (SpecSys)
@@ -361,9 +361,8 @@ struct
     in
 
     let print_globals glob =
-      let out = M.get_out (Spec.name ()) !M.out in
       let print_one v st =
-        ignore (Pretty.fprintf out "%a -> %a\n" EQSys.GVar.pretty_trace v EQSys.G.pretty st)
+        ignore (Pretty.fprintf !M.out "%a -> %a\n" EQSys.GVar.pretty_trace v EQSys.G.pretty st)
       in
       GHT.iter print_one glob
     in

src/framework/xsltResultOutput.ml

@@ -78,7 +78,6 @@ struct
 
   let output table live gtable gtfxml (module FileCfg: MyCFG.FileCfg) =
     let file = FileCfg.file in
-    let out = Messages.get_out result_name !Messages.out in
     let module SH = BatHashtbl.Make (Basetype.RawStrings) in
     let file2funs = SH.create 100 in
     let funs2node = SH.create 100 in
@@ -121,7 +120,7 @@ struct
       do_html_output xml_file_name
     )
     else
-      let f = BatIO.output_channel out in
+      let f = BatIO.output_channel !Messages.out in
       ignore (write_file f (get_string "outfile"))
 end
 

src/maingoblint.ml

@@ -192,13 +192,7 @@ let handle_flags () =
     set_auto "lib.activated[+]" "sv-comp";
 
   if get_bool "kernel" then
-    set_auto "lib.activated[+]" "linux-kernel";
-
-  match get_string "dbg.dump" with
-  | "" -> ()
-  | path ->
-    Messages.formatter := Format.formatter_of_out_channel (open_out (Legacy.Filename.concat path "warnings.out"));
-    set_string "outfile" ""
+    set_auto "lib.activated[+]" "linux-kernel"
 
 let handle_options () =
   Logs.Level.current := Logs.Level.of_string (get_string "dbg.level");
@@ -490,7 +484,7 @@ let merge_parsed parsed =
     if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")
   in
 
-  Errormsg.logChannel := Messages.get_out "cil" cilout;
+  Errormsg.logChannel := cilout;
 
   (* we use CIL to merge all inputs to ONE file *)
   let merged_AST =
@@ -523,7 +517,7 @@ let do_stats () =
     Goblint_solver.SolverStats.print ();
     Logs.newline ();
     Logs.info "Timings:";
-    Timing.Default.print (Stdlib.Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr);
+    Timing.Default.print (Stdlib.Format.formatter_of_out_channel Legacy.stderr);
     flush_all ()
   )