diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-14 21:41:44 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-14 21:41:44 +0100 |
commit | 0dd01dbafe5125d69562640534fca6fe79fa9d82 (patch) | |
tree | 4cea42ac773aa4c27dcf25796adf9c0a9ca7642a /mppa_k1c | |
parent | 03f2891a533dccbd8e4b5ba58a734fee79f1dd06 (diff) | |
download | compcert-kvx-0dd01dbafe5125d69562640534fca6fe79fa9d82.tar.gz compcert-kvx-0dd01dbafe5125d69562640534fca6fe79fa9d82.zip |
better robustness wrt exceptions
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/InstructionScheduler.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/mppa_k1c/InstructionScheduler.ml b/mppa_k1c/InstructionScheduler.ml index ce687678..dca4b8ff 100644 --- a/mppa_k1c/InstructionScheduler.ml +++ b/mppa_k1c/InstructionScheduler.ml @@ -1107,16 +1107,20 @@ let ilp_read_solution mapper channel = let ilp_solver = ref "ilp_solver" let problem_nr = ref 0 - + +let do_with_resource destroy x f = + try + let r = f x in + destroy x; r + with exn -> destroy x; 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 = do_with_resource close_out (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 | Unix.WEXITED 0 -> |