diff options
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ceee1810..46b788fe 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -903,14 +903,12 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: match lmb with | nil => OK nil | mb :: lmb => - do lb <- transl_block f mb ep; + do lb <- transl_block f mb (if Machblock.header mb then ep else false); do lb' <- transl_blocks f lmb false; OK (lb ++ lb') end . - - Definition transl_function (f: Machblock.function) := do lb <- transl_blocks f f.(Machblock.fn_code) true; OK (mkfunction f.(Machblock.fn_sig) |