From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 12:50:57 +0000 Subject: Added support for jump tables in back end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgen.v | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) (limited to 'powerpc/Asmgen.v') diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index aebb4834..4beabb1c 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -502,6 +502,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := let p := crbit_for_cond cond in transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) + | Mjumptable arg tbl => + Pbtbl (ireg_of arg) tbl :: k | Mreturn => Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR12 :: @@ -523,17 +525,11 @@ Definition transl_function (f: Mach.function) := Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: transl_code f f.(fn_code). -Fixpoint code_size (c: code) : Z := - match c with - | nil => 0 - | instr :: c' => code_size c' + 1 - end. - Open Local Scope string_scope. Definition transf_function (f: Mach.function) : res Asm.code := let c := transl_function f in - if zlt Int.max_unsigned (code_size c) + if zlt Int.max_unsigned (list_length_z c) then Errors.Error (msg "code size exceeded") else Errors.OK c. -- cgit