From 89a0a0e4acc6ea895a3eb702be88caf42c7096f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 May 2019 18:48:24 +0200 Subject: gain d'un cycle au moment du freeframe (passer au ret dans le même bundle) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asm.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 -- cgit