Use OCaml 4.14 features: TRMC, In_channel, Out_channel, Seq.uncons

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c1370c59-ec35-42df-b0d5-d48a7f47e2f2

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

Author: Copilot

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -7,7 +7,9 @@ module BISet = struct
   let is_singleton s = cardinal s = 1
 
   let map_reduce f g s =
-    s |> to_seq |> Seq.map f |> BatSeq.reduce g
+    match s |> to_seq |> Seq.map f |> Seq.uncons with
+    | None -> invalid_arg "BISet.map_reduce"
+    | Some (x, rest) -> Seq.fold_left g x rest
 end
 
 (* The module [Exclusion] constains common functionality about handling of exclusion sets between [DefExc] and [Enums] *)

src/common/util/messages.ml

@@ -184,7 +184,7 @@ let out = ref stdout
 
 let get_out name alternative = match get_string "dbg.dump" with
   | "" -> alternative
-  | path -> open_out (Filename.concat path (name ^ ".out"))
+  | path -> Out_channel.open_text (Filename.concat path (name ^ ".out"))
 
 
 let print ?(ppf= !formatter) (m: Message.t) =

src/incremental/makefileUtil.ml

@@ -2,8 +2,6 @@
 
 open Unix
 
-let buff_size = 1024
-
 (* Suffix of files combined by CIL *)
 let comb_suffix = "_comb.c"
 
@@ -16,18 +14,10 @@ let exec_command ?path (command: string) =
     ) path;
   Logs.debug "%s" ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ());
   let (std_out, std_in) = open_process command in
-  let output = Buffer.create buff_size in
-  try
-    while true do
-      let line = input_char std_out in
-      Buffer.add_char output line
-    done;
-    assert false;
-  with End_of_file ->
-    let exit_code = close_process (std_out,std_in) in
-    let output = Buffer.contents output in
-    Sys.chdir current_dir;
-    (exit_code, output)
+  let output = In_channel.input_all std_out in
+  let exit_code = close_process (std_out, std_in) in
+  Sys.chdir current_dir;
+  (exit_code, output)
 
 
 (* BFS for a file with a given suffix in a directory or any subdirectoy *)

src/maingoblint.ml

@@ -197,7 +197,7 @@ let handle_flags () =
   match get_string "dbg.dump" with
   | "" -> ()
   | path ->
-    Messages.formatter := Format.formatter_of_out_channel (open_out (Legacy.Filename.concat path "warnings.out"));
+    Messages.formatter := Format.formatter_of_out_channel (Out_channel.open_text (Filename.concat path "warnings.out"));
     set_string "outfile" ""
 
 let handle_options () =
@@ -487,7 +487,7 @@ let parse_preprocessed preprocessed =
 (** Merge parsed files *)
 let merge_parsed parsed =
   let cilout =
-    if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")
+    if get_string "dbg.cilout" = "" then Out_channel.stderr else Out_channel.open_text (get_string "dbg.cilout")
   in
 
   Errormsg.logChannel := Messages.get_out "cil" cilout;
@@ -523,7 +523,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 @@ Messages.get_out "timing" Out_channel.stderr);
     flush_all ()
   )
 
@@ -536,9 +536,9 @@ let reset_stats () =
 let do_analyze change_info merged_AST =
   (* direct the output to file if requested  *)
   if get_string "outfile" <> "" then (
-    if !Messages.out <> Legacy.stdout then
-      Legacy.close_out !Messages.out;
-    Messages.out := Legacy.open_out (get_string "outfile"));
+    if !Messages.out <> Out_channel.stdout then
+      Out_channel.close !Messages.out;
+    Messages.out := Out_channel.open_text (get_string "outfile"));
 
   let module L = Printable.Liszt (CilType.Fundec) in
   if get_bool "justcil" then

src/solver/generic.ml

@@ -106,9 +106,9 @@ struct
     if save_run_str <> "" then (
       let save_run = Fpath.v save_run_str in
       GobSys.mkdir_or_exists save_run;
-      Fpath.(to_string (save_run / "solver_stats.csv")) |> open_out |> Option.some
+      Fpath.(to_string (save_run / "solver_stats.csv")) |> Out_channel.open_text |> Option.some
     ) else None
-  let write_csv xs oc = output_string oc @@ String.concat ",\t" xs ^ "\n"
+  let write_csv xs oc = Out_channel.output_string oc @@ String.concat ",\t" xs ^ "\n"
 
   (* print generic and specific stats *)
   let print_stats _ =
@@ -123,7 +123,7 @@ struct
     Logs.newline ();
     (* Timing.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *)
     (* Gc.print_stat stdout; (* too verbose, slow and words instead of MB *) *)
-    let gc = GobGc.print_quick_stat Legacy.stderr in
+    let gc = GobGc.print_quick_stat Out_channel.stderr in
     Logs.newline ();
     Option.may (write_csv [GobSys.string_of_time (); string_of_int !SolverStats.vars; string_of_int !SolverStats.evals; string_of_int !ncontexts; string_of_int gc.Gc.top_heap_words]) stats_csv
     (* print_string "Do you want to continue? [Y/n]"; *)

src/util/std/gobList.ml

@@ -1,7 +1,7 @@
 open Batteries
 
 (** The normal haskell zip that throws no exception *)
-let rec combine_short l1 l2 = match l1, l2 with
+let[@tail_mod_cons] rec combine_short l1 l2 = match l1, l2 with
   | x1 :: l1, x2 :: l2 -> (x1, x2) :: combine_short l1 l2
   | _, _ -> []