things start to compile C

1 files changed, 5 insertions, 6 deletions

diff --git a/backend/RTLblockrevgen.v b/backend/RTLblockrevgen.v
index 13f17d58..9e208b8d 100644
--- a/backend/RTLblockrevgen.v
+++ b/backend/RTLblockrevgen.v
@@ -21,13 +21,13 @@ Definition set_node (ns : nodestate)  (node : RTL.node) (insn : RTL.instruction)
   (mknodestate (ns_next_node ns)
                (ns_label2node ns) 
                (PTree.set node insn (ns_code ns))).
-
+(*
 Definition alloc_node (ns : nodestate) : nodestate * RTL.node :=
   ((mknodestate (Pos.succ (ns_next_node ns))
                 (ns_label2node ns)
                 (ns_code ns)),
    (ns_next_node ns)).
-
+*)
 Definition fresh_node (ns : nodestate) (insn : RTL.instruction) :
   nodestate * RTL.node :=
   ((mknodestate (Pos.succ (ns_next_node ns))
@@ -130,7 +130,7 @@ Fixpoint transl_code
       match PTree.get label code with
       | None => Error (Errors.msg "RTLblockrevgen.transl_code: cannot find block for label")
       | Some block =>
-        let (ns', head_node) := alloc_node ns in
+        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'
@@ -142,11 +142,10 @@ Definition transl_function (fn : RTLblock.function): Errors.res (RTL.function) :
   do ns <- transl_code initial_nodestate (RTLblock.fn_code fn)
      (RTLblock.fn_entrypoint fn :: nil) 300%nat ;
     match PTree.get (RTLblock.fn_entrypoint fn) (ns_label2node ns) with
-    | None => Error (Errors.msg "RTLblockrevgen.transl_function: cannot find entrypoint")
+    | None =>  Error (Errors.msg "RTLblockrevgen.transl_function: cannot find entrypoint")
     | Some entrypoint =>
       OK (RTL.mkfunction (RTLblock.fn_sig fn) (RTLblock.fn_params fn)
-                         (RTLblock.fn_stacksize fn) (ns_code ns) entrypoint
-         )
+                         (RTLblock.fn_stacksize fn) (ns_code ns) entrypoint)
     end.