aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Duplicateaux.ml
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-12-16 16:55:40 +0100
committerCyril SIX <cyril.six@kalray.eu>2019-12-16 16:55:40 +0100
commitaed1bf936b69464f99a92133a43d51664295d780 (patch)
treec3e2f11396f4a14a075586ed73b49be889da6983 /backend/Duplicateaux.ml
parent26775340b173fd631e850f0a553ddab25c934fbc (diff)
downloadcompcert-kvx-aed1bf936b69464f99a92133a43d51664295d780.tar.gz
compcert-kvx-aed1bf936b69464f99a92133a43d51664295d780.zip
Opcode heuristic done for K1c
Diffstat (limited to 'backend/Duplicateaux.ml')
-rw-r--r--backend/Duplicateaux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 1fecd0d9..a987d73f 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -261,7 +261,7 @@ let get_directions code entrypoint =
do_loop_heuristic code ifso ifnot is_loop_header preferred;
Printf.printf "Random choice for %d\n" (P.to_int n);
preferred := Random.bool ()
- with HeuristicSucceeded -> ()
+ with HeuristicSucceeded | DuplicateOpcodeHeuristic.HeuristicSucceeded -> ()
); directions := PTree.set n !preferred !directions
| _ -> ()
) bfs_order;