aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-01-22 16:22:44 +0100
committerCyril SIX <cyril.six@kalray.eu>2020-01-22 16:22:44 +0100
commit60c15c9d1105dc2e53c17b3fb28ee9cc4716cbc6 (patch)
treeb35f53c04212f43ed554073cd449cca4be3bcc73
parentd3cd82c2c82727e7fb76e95e5dcce6cfa9055015 (diff)
downloadcompcert-kvx-60c15c9d1105dc2e53c17b3fb28ee9cc4716cbc6.tar.gz
compcert-kvx-60c15c9d1105dc2e53c17b3fb28ee9cc4716cbc6.zip
Fixing is_empty function
-rw-r--r--backend/Duplicateaux.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 3dfc7969..66c57cda 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -481,8 +481,8 @@ let rec maxint = function
| i :: l -> assert (i >= 0); let m = maxint l in if i > m then i else m
let is_empty = function
- | [] -> false
- | _ -> true
+ | [] -> true
+ | _ -> false
(* code: RTL code
* preds: mapping node -> predecessors
@@ -506,7 +506,7 @@ let tail_duplicate code preds ptree trace =
in let final_node_preds = match !last_duplicate with
| None -> node_preds_nolast
| Some n' -> n' :: node_preds_nolast
- in if is_empty final_node_preds then
+ in if not (is_empty final_node_preds) then
let n' = !next_int
in let (newc, newp) = duplicate code ptree !last_node n final_node_preds (P.of_int n')
in begin