diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-08-31 18:48:29 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-08-31 18:48:29 +0200 |
commit | 6f12f83d4109943e6c4df780dccf0740e2437c7f (patch) | |
tree | 67baa79c389cd73119ddeddf23a601033ccc1dd3 | |
parent | e069f9abea7cdb2fb088a30ac24668aa4973269e (diff) | |
download | compcert-kvx-6f12f83d4109943e6c4df780dccf0740e2437c7f.tar.gz compcert-kvx-6f12f83d4109943e6c4df780dccf0740e2437c7f.zip |
fix problem with some file descriptors possibly never getting closed
(need to propagate fix to other kinds of solvers)
-rw-r--r-- | kvx/InstructionScheduler.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/kvx/InstructionScheduler.ml b/kvx/InstructionScheduler.ml index e4dc3f97..307e637e 100644 --- a/kvx/InstructionScheduler.ml +++ b/kvx/InstructionScheduler.ml @@ -1193,15 +1193,21 @@ let ilp_read_solution mapper channel = let ilp_solver = ref "ilp_solver" let problem_nr = ref 0 - + +let with_out_channel chan f = + try let ret = f chan in + close_out chan; + ret + with exn -> close_out chan; + raise exn;; + let ilp_scheduler pb_type problem = try let filename_in = Printf.sprintf "problem%05d.lp" !problem_nr and filename_out = Printf.sprintf "problem%05d.sol" !problem_nr in incr problem_nr; - let opb_problem = open_out filename_in in - let mapper = ilp_print_problem opb_problem problem pb_type in - close_out opb_problem; + let mapper = with_out_channel (open_out filename_in) + (fun opb_problem -> ilp_print_problem opb_problem problem pb_type) in begin match Unix.system (!ilp_solver ^ " " ^ filename_in ^ " " ^ filename_out) with |