diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml index c3ac7d1d2c..f88004056f 100644 --- a/src/common/util/messages.ml +++ b/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 diff --git a/src/config/options.schema.json b/src/config/options.schema.json index c002dfa88e..18ea9f4716 100644 --- a/src/config/options.schema.json +++ b/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", diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml index 2d9fe623c7..a67632d294 100644 --- a/src/framework/analysisResult.ml +++ b/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 diff --git a/src/framework/analysisResultOutput.ml b/src/framework/analysisResultOutput.ml index 29f2006f8e..45c39abfa1 100644 --- a/src/framework/analysisResultOutput.ml +++ b/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)) diff --git a/src/framework/control.ml b/src/framework/control.ml index 40b753f0fa..c5e5e12d1c 100644 --- a/src/framework/control.ml +++ b/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 diff --git a/src/framework/xsltResultOutput.ml b/src/framework/xsltResultOutput.ml index 3f8cdaed1c..2fe63e9e03 100644 --- a/src/framework/xsltResultOutput.ml +++ b/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 diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 6584ac7c82..3522742964 100644 --- a/src/maingoblint.ml +++ b/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 () )