Skip to content
Open
Show file tree
Hide file tree
Changes from all 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
5 changes: 2 additions & 3 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2031,12 +2031,11 @@ struct
v

let dump () =
let f = open_out_bin (get_string "exp.priv-prec-dump") in
Out_channel.with_open_bin (get_string "exp.priv-prec-dump") @@ fun f ->
(* LVH.iter (fun (l, x) v ->
Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty x VD.pretty v
) lvh; *)
Marshal.output f ({name = get_string "ana.base.privatization"; results = lvh}: result);
close_out_noerr f
Stdlib.Marshal.to_channel f ({name = get_string "ana.base.privatization"; results = lvh}: result) []

let finalize () =
if !is_dumping then
Expand Down
8 changes: 3 additions & 5 deletions src/common/framework/cfgTools.ml
Original file line number Diff line number Diff line change
Expand Up @@ -600,12 +600,11 @@ let fprint_hash_dot cfg =
let extraNodeStyles node = []
end
in
let out = open_out "cfg.dot" in
Out_channel.with_open_text "cfg.dot" @@ fun out ->
let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfg in
let ppf = Format.formatter_of_out_channel out in
fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges ppf;
Format.pp_print_flush ppf ();
close_out out
Format.pp_print_flush ppf ()


let getCFG (file: file) : cfg * cfg * _ =
Expand Down Expand Up @@ -664,11 +663,10 @@ let dead_code_cfg ~path (module FileCfg: MyCFG.FileCfg) live =
let dot_file_name = fd.svar.vname^".dot" in
let file_dir = GobSys.mkdir_or_exists_absolute Fpath.(base_dir / c_file_name) in
let fname = Fpath.(file_dir / dot_file_name) in
let out = open_out (Fpath.to_string fname) in
Out_channel.with_open_text (Fpath.to_string fname) @@ fun out ->
let ppf = Format.formatter_of_out_channel out in
fprint_fundec_html_dot (module FileCfg.Cfg) live fd ppf;
Format.pp_print_flush ppf ();
close_out out
| _ -> ()
)

Expand Down
9 changes: 1 addition & 8 deletions src/config/gobConfig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -415,14 +415,7 @@ struct
in
match file with
| Some fn ->
let v =
let ic = Stdlib.open_in (Fpath.to_string fn) in
Fun.protect ~finally:(fun () ->
Stdlib.close_in ic
) (fun () ->
Yojson.Safe.from_channel ic
)
in
let v = In_channel.with_open_text (Fpath.to_string fn) Yojson.Safe.from_channel in
merge v;
if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a." GobFpath.pretty fn GobYojson.pretty !json_conf
| None -> raise (Sys_error (Printf.sprintf "%s: No such file or directory" (Fpath.to_string fn)))
Expand Down
11 changes: 5 additions & 6 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
Expand Up @@ -582,7 +582,9 @@ struct
end
in
(* Yojson.Safe.to_file meta Meta.json; *)
Yojson.Safe.pretty_to_channel (Stdlib.open_out (Fpath.to_string meta)) Meta.json; (* the above is compact, this is pretty-printed *)
Out_channel.with_open_text (Fpath.to_string meta) (fun oc ->
Yojson.Safe.pretty_to_channel oc Meta.json (* the above is compact, this is pretty-printed *)
);
if gobview then (
Logs.Format.debug "Saving the analysis table to %a, the CIL state to %a, the warning table to %a, and the runtime stats to %a" Fpath.pp analyses Fpath.pp cil Fpath.pp warnings Fpath.pp stats;
Serialize.marshal MCPRegistry.registered_name analyses;
Expand Down Expand Up @@ -789,13 +791,10 @@ struct
end
in
let module ArgDot = ArgTools.Dot (Arg) (NoLabelNodeStyle) in
let oc = Batteries.open_out arg_dot_path in
Fun.protect (fun () ->
let ppf = Format.formatter_of_out_channel oc in
Out_channel.with_open_text arg_dot_path (fun oc ->
let ppf = Stdlib.Format.formatter_of_out_channel oc in
ArgDot.dot ppf;
Format.pp_print_flush ppf ()
) ~finally:(fun () ->
Batteries.close_out oc
)
);
ArgTools.current_arg := Some (module Arg);
Expand Down
9 changes: 3 additions & 6 deletions src/incremental/serialize.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
(** Serialization/deserialization of incremental analysis data. *)

open Batteries

(* TODO: GoblintDir *)
let incremental_data_file_name = "analysis.data"
let results_dir = "results"
Expand All @@ -22,13 +20,12 @@ let gob_results_dir op =
let server () = GobConfig.get_bool "server.enabled"

let marshal obj fileName =
let chan = open_out_bin (Fpath.to_string fileName) in
Marshal.output chan obj;
close_out chan
Out_channel.with_open_bin (Fpath.to_string fileName) @@ fun chan ->
Marshal.to_channel chan obj []

let unmarshal fileName =
Logs.debug "Unmarshalling %s... If type of content changed, this will result in a segmentation fault!" (Fpath.to_string fileName);
Marshal.input (open_in_bin (Fpath.to_string fileName))
In_channel.with_open_bin (Fpath.to_string fileName) Marshal.from_channel

let results_exist () =
(* If Goblint did not crash irregularly, the existence of the result directory indicates that there are results *)
Expand Down
3 changes: 1 addition & 2 deletions src/solver/sLR.ml
Original file line number Diff line number Diff line change
Expand Up @@ -481,7 +481,7 @@ module PrintInfluence =
struct
module S1 = Sol (S) (HM)
let solve x y =
let ch = Legacy.open_out "test.dot" in
Out_channel.with_open_text "test.dot" @@ fun ch ->
let r = S1.solve x y in
let f k _ =
let q = if HM.mem S1.wpoint k then " shape=box style=rounded" else "" in
Expand All @@ -498,7 +498,6 @@ module PrintInfluence =
ignore (Pretty.fprintf ch "digraph G {\nedge [arrowhead=vee];\n");
HM.iter f r;
ignore (Pretty.fprintf ch "}\n");
Legacy.close_out_noerr ch;
r
end

Expand Down
5 changes: 2 additions & 3 deletions src/transform/transform.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,10 +37,9 @@ let run_transformations ?(file_output = true) file names ask =

if file_output && List.exists (fun (_, (module T : S)) -> T.requires_file_output) active_transformations then
let filename = GobConfig.get_string "trans.output" in
let oc = Stdlib.open_out filename in
Out_channel.with_open_text filename @@ fun oc ->
GobRef.wrap GoblintCil.lineDirectiveStyle None @@ fun () ->
dumpFile defaultCilPrinter oc filename file;
Stdlib.close_out oc
dumpFile defaultCilPrinter oc filename file

let run file name = run_transformations ~file_output:false file [name]

Expand Down
4 changes: 1 addition & 3 deletions src/util/precCompare.ml
Original file line number Diff line number Diff line change
Expand Up @@ -95,10 +95,8 @@ struct
open Util

let load filename =
let f = open_in_bin filename in
let dump: dump = Marshal.from_channel f in
let dump: dump = In_channel.with_open_bin filename Stdlib.Marshal.from_channel in
let dump: result = {name = dump.name; results = unmarshal dump.marshalled } in
close_in_noerr f;
dump

module CompareDump = MakeHashtbl (Key) (Dom) (RH)
Expand Down
3 changes: 1 addition & 2 deletions tests/regression/cfg/util/cfgDot.ml
Original file line number Diff line number Diff line change
Expand Up @@ -87,12 +87,11 @@ let main () =

GoblintCil.iterGlobals ast (function
| GFun (fd, _) ->
let out = open_out (fd.svar.vname ^ ".dot") in
Out_channel.with_open_text (fd.svar.vname ^ ".dot") @@ fun out ->
let iter_edges = CfgTools.iter_fd_edges (module Cfg) fd in
let ppf = Format.formatter_of_out_channel out in
CfgTools.fprint_dot (module CfgTools.CfgPrinters (LocationExtraNodeStyles)) iter_edges ppf;
Format.pp_print_flush ppf ();
close_out out
| _ -> ()
)

Expand Down
Loading