diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-18 22:37:01 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-18 22:37:01 +0200 |
| commit | 300e51261c090e6a66bd0e0004bb530b64caf6e9 (patch) | |
| tree | ec00ecf7ff0476811265caf24b6788b3815f2147 /backend/LICMaux.ml | |
| parent | 2efb64e96105c90f68f22a0a0bc386d1ac039354 (diff) | |
| download | compcert-kvx-300e51261c090e6a66bd0e0004bb530b64caf6e9.tar.gz compcert-kvx-300e51261c090e6a66bd0e0004bb530b64caf6e9.zip | |
pp_list
Diffstat (limited to 'backend/LICMaux.ml')
| -rw-r--r-- | backend/LICMaux.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index ecc11a00..39e336eb 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -107,17 +107,20 @@ let inner_loops (f : coq_function) : PSet.t PTree.t = and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in PTree.map (filter_dominated_part predecessors) parts;; -let pp_pset oc s = +let pp_list pp_item oc l = output_string oc "{ "; let first = ref true in List.iter (fun x -> (if !first then first := false else output_string oc ", "); - Printf.printf "%d" x) - (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s))); + pp_item oc x) l; output_string oc " }";; +let pp_pset oc s = + pp_list (fun oc -> Printf.fprintf oc "%d") oc + (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s)));; + let print_dominated_parts oc f = List.iter (fun (header, nodes) -> Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) |