diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 12:50:57 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 12:50:57 +0000 |
| commit | 74487f079dd56663f97f9731cea328931857495c (patch) | |
| tree | 9de10b895da39adffaf66bff983d6ed573898068 /powerpc/Asmgen.v | |
| parent | 0486654fac91947fec93d18a0738dd7aa10bcf96 (diff) | |
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
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index aebb483..4beabb1 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. |