diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-07 18:48:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-07 18:48:24 +0200 |
| commit | 89a0a0e4acc6ea895a3eb702be88caf42c7096f8 (patch) | |
| tree | 14496ac08e9f4d7d8a923e868c2bf7546171d5ce /mppa_k1c/Asm.v | |
| parent | 9fe593b2b3871d59b87fa0cf472693636626d32f (diff) | |
| download | compcert-kvx-89a0a0e4acc6ea895a3eb702be88caf42c7096f8.tar.gz compcert-kvx-89a0a0e4acc6ea895a3eb702be88caf42c7096f8.zip | |
gain d'un cycle au moment du freeframe (passer au ret dans le même bundle)
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index b928a48e..1774b102 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -518,7 +518,12 @@ Definition unfold_exit (oc: option control) := | Some c => control_to_instruction c :: nil
end.
-Definition unfold_bblock (b: bblock) := unfold_label (header b) ++ unfold_body (body b) ++ unfold_exit (exit b) ++ Psemi :: nil.
+Definition unfold_bblock (b: bblock) := unfold_label (header b) ++
+ (match (body b), (exit b) with
+ | (((Asmvliw.Pfreeframe _ _ | Asmvliw.Pallocframe _ _)::nil) as bo), None =>
+ unfold_body bo
+ | bo, ex => unfold_body bo ++ unfold_exit ex ++ Psemi :: nil
+ end).
Fixpoint unfold (lb: bblocks) :=
match lb with
|