diff options
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 0124bf63..e1a38c45 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -327,15 +327,8 @@ Definition unfold_bblock (bb: bblock) := * basic block. *) if zle (list_length_z (header bb)) 1 then - do rest <- (match (body bb), (exit bb) with - | (((Asmblock.Pfreeframe _ _ - | Asmblock.Pallocframe _ _)::nil) as bo), None => - unfold_body bo - | bo, ex => - do bo_is <- unfold_body bo; - OK (bo_is ++ unfold_exit ex) - end) - ; OK (lbl ++ rest) + do bo_is <- unfold_body (body bb); + OK (lbl ++ bo_is ++ unfold_exit (exit bb)) else Error (msg "Asmgen.unfold_bblock: Multiple labels were generated."). |