loops now work

1 files changed, 11 insertions, 10 deletions

diff --git a/backend/RTLblockrevgen.v b/backend/RTLblockrevgen.v
index 694616b7..313bc305 100644
--- a/backend/RTLblockrevgen.v
+++ b/backend/RTLblockrevgen.v
@@ -113,13 +113,9 @@ Definition transl_cfi (ns : nodestate) (cfi : RTLblock.cfinstruction)
 
 Definition transl_block (ns : nodestate) (block : RTLblock.block)
            (head_node : RTL.node) : nodestate :=
-  match PTree.get head_node (ns_code ns) with
-  | Some _ => ns
-  | None =>
-    let (ns', next_insn) := transl_cfi ns (blk_control block) in
-    transl_block_revbody ns' (List.rev (blk_insns block))
-                         head_node next_insn
-  end.
+  let (ns', next_insn) := transl_cfi ns (blk_control block) in
+  transl_block_revbody ns' (List.rev (blk_insns block))
+                       head_node next_insn.
 
 Fixpoint transl_code
   (ns : nodestate)
@@ -137,9 +133,14 @@ Fixpoint transl_code
       | None => Error (Errors.msg "RTLblockrevgen.transl_code: cannot find block for label")
       | Some block =>
         let (ns', head_node) := get_target ns label in
-        transl_code (transl_block ns' block head_node) code
-                    (cfi_targets (blk_control block) ++ rest_labels)
-                    max_size'
+        match PTree.get head_node (ns_code ns) with
+        | Some _ =>
+          transl_code ns' code rest_labels max_size'
+        | None =>
+          transl_code (transl_block ns' block head_node) code
+                      (cfi_targets (blk_control block) ++ rest_labels)
+                      max_size'
+        end
       end
     end
   end.