diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 12:18:40 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 12:18:40 +0100 |
commit | 65464e2b1623f9fa725f4503d0f78ac2a502a4fb (patch) | |
tree | 9bc4bf3e20c7a393c93c19d9562f0ccabed11d43 | |
parent | 215d550f2154ae39506a19ee440cf7248367ea0a (diff) | |
download | compcert-kvx-65464e2b1623f9fa725f4503d0f78ac2a502a4fb.tar.gz compcert-kvx-65464e2b1623f9fa725f4503d0f78ac2a502a4fb.zip |
things start to compile C
-rw-r--r-- | backend/RTLblockrevgen.v | 11 |
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. |