aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Duplicateaux.ml
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-01-24 13:48:45 +0100
committerCyril SIX <cyril.six@kalray.eu>2020-01-24 13:48:45 +0100
commit8aa9cb8c221ad4f2d27a7c54eca256bc70425aff (patch)
treeebe416934cb53beb963b450ab584a898148dca66 /backend/Duplicateaux.ml
parentd69de4bcef55cb9c35acba1cc01b0b198a15008e (diff)
downloadcompcert-kvx-8aa9cb8c221ad4f2d27a7c54eca256bc70425aff.tar.gz
compcert-kvx-8aa9cb8c221ad4f2d27a7c54eca256bc70425aff.zip
Added debug message when inverting ifso ifnot
Diffstat (limited to 'backend/Duplicateaux.ml')
-rw-r--r--backend/Duplicateaux.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index a974133e..a553a370 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -541,7 +541,9 @@ let rec invert_iconds_trace code = function
let code' = match ptree_get_some n code with
| Icond (c, lr, ifso, ifnot) ->
assert (n' == ifso || n' == ifnot);
- if (n' == ifso) then PTree.set n (Icond (Op.negate_condition c, lr, ifnot, ifso)) code
+ if (n' == ifso) then (
+ Printf.printf "Reversing ifso/ifnot for node %d\n" (P.to_int n);
+ PTree.set n (Icond (Op.negate_condition c, lr, ifnot, ifso)) code )
else code
| _ -> code
in invert_iconds_trace code' (n'::t)