diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 21:35:25 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 21:35:25 +0100 |
| commit | d47f93b0f7ced7ae02cfeb8827886ac65e06817d (patch) | |
| tree | 9cb468148b5d640682bfe29a3e0e9e7d9a9a41ec /backend/CSE3analysisaux.ml | |
| parent | e3e33a26c5ddb7c7747da67aa36fd56d0386f3c8 (diff) | |
| download | compcert-kvx-d47f93b0f7ced7ae02cfeb8827886ac65e06817d.tar.gz compcert-kvx-d47f93b0f7ced7ae02cfeb8827886ac65e06817d.zip | |
-fcse3 command line option
Diffstat (limited to 'backend/CSE3analysisaux.ml')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 8229a76d..2e7d7063 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -24,8 +24,7 @@ let string_of_chunk = function let print_reg channel i = Printf.fprintf channel "r%d" i;; -let print_eq channel id (lhs, sop, args) = - Printf.printf "%d: " id; +let print_eq channel (lhs, sop, args) = match sop with | SOp op -> Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args) @@ -50,13 +49,14 @@ let preanalysis (f : RTL.coq_function) = let mutating_eq_find_oracle node eq : P.t option = let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in match Hashtbl.find_opt eq_table flat_eq with - | Some x -> Some x + | Some x -> + Some x | None -> + (* FIXME print_eq stderr flat_eq; *) incr cur_eq_id; let id = !cur_eq_id in let coq_id = P.of_int id in begin - print_eq stderr id flat_eq; Hashtbl.add eq_table flat_eq coq_id; Hashtbl.add rhs_table (flat_eq_op, flat_eq_args) (PSet.add coq_id |