diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-22 17:29:56 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-22 17:29:56 +0100 |
| commit | 5ce9d33ddf09747ce6cf6e3bea70097556b454f4 (patch) | |
| tree | c9389f1276ff655e2cd9d1360c95f4218dc4dba9 | |
| parent | 89e029310d175ee7ddbb157494bac46a08304b19 (diff) | |
| download | compcert-kvx-5ce9d33ddf09747ce6cf6e3bea70097556b454f4.tar.gz compcert-kvx-5ce9d33ddf09747ce6cf6e3bea70097556b454f4.zip | |
Fixing bug (used physical instead of structural inequality)
| -rw-r--r-- | backend/Duplicateaux.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 66c57cda..67fbf3ad 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -468,6 +468,7 @@ let rec change_pointers code n n' = function * n': the integer which should contain the duplicate of n * returns: new code, new ptree *) let duplicate code ptree parent n preds n' = + Printf.printf "Duplicating node %d into %d..\n" (P.to_int n) (P.to_int n'); match PTree.get n' code with | Some _ -> failwith "The PTree already has a node n'" | None -> @@ -502,7 +503,7 @@ let tail_duplicate code preds ptree trace = if is_first then (code, ptree) (* first node is never duplicated regardless of its inputs *) else let node_preds = ptree_get_some n preds - in let node_preds_nolast = List.filter (fun e -> e != get_some !last_node) node_preds + in let node_preds_nolast = List.filter (fun e -> e <> get_some !last_node) node_preds in let final_node_preds = match !last_duplicate with | None -> node_preds_nolast | Some n' -> n' :: node_preds_nolast |