From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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
---
 backend/Reload.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backend/Reload.v')

diff --git a/backend/Reload.v b/backend/Reload.v
index 621e75b5..5728a628 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -242,6 +242,9 @@ Definition transf_instr
   | LTLin.Lcond cond args lbl =>
       let rargs := regs_for args in
       add_reloads args rargs (Lcond cond rargs lbl :: k)
+  | LTLin.Ljumptable arg tbl =>
+      let rarg := reg_for arg in
+      add_reload arg rarg (Ljumptable rarg tbl :: k)
   | LTLin.Lreturn None =>
       Lreturn :: k
   | LTLin.Lreturn (Some loc) =>
-- 
cgit