Skip to content
Open
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 0 additions & 4 deletions src/common/util/messages.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 0 additions & 6 deletions src/config/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
2 changes: 1 addition & 1 deletion src/framework/analysisResultOutput.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
3 changes: 1 addition & 2 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions src/framework/xsltResultOutput.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -122,7 +121,7 @@ struct
do_html_output !xml_file_name
)
else
let f = BatIO.output_channel out in
let f = BatIO.output_channel !Messages.out in
write_file f (get_string "outfile")
end

Expand Down
12 changes: 3 additions & 9 deletions src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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 ()
)

Expand Down
Loading