diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 16:07:19 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 16:07:19 +0100 |
| commit | 164740efbdcf3053520926c9d7ddfd33b673a808 (patch) | |
| tree | 05b51ec90cb57593537ec71fbc12a025fa7a9aeb | |
| parent | 1f862e1e61ac9b52509e6843bb3948e0a0b2c770 (diff) | |
| download | compcert-kvx-164740efbdcf3053520926c9d7ddfd33b673a808.tar.gz compcert-kvx-164740efbdcf3053520926c9d7ddfd33b673a808.zip | |
deal with loops properly
| -rw-r--r-- | backend/RTLblockrevgen.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/backend/RTLblockrevgen.v b/backend/RTLblockrevgen.v index ca61e8ee..694616b7 100644 --- a/backend/RTLblockrevgen.v +++ b/backend/RTLblockrevgen.v @@ -113,9 +113,14 @@ Definition transl_cfi (ns : nodestate) (cfi : RTLblock.cfinstruction) Definition transl_block (ns : nodestate) (block : RTLblock.block) (head_node : RTL.node) : nodestate := - let (ns', next_insn) := transl_cfi ns (blk_control block) in - transl_block_revbody ns' (List.rev (blk_insns block)) - head_node next_insn. + 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. + Fixpoint transl_code (ns : nodestate) (code : RTLblock.code) |