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/Allocation.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'backend/Allocation.v')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 7d843e57..b802f4ac 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -103,6 +103,8 @@ Definition transfer
 	  reg_list_live args (reg_sum_live ros Regset.empty)
       | Icond cond args ifso ifnot =>
           reg_list_live args after
+      | Ijumptable arg tbl =>
+          reg_live arg after
       | Ireturn optarg =>
           reg_option_live optarg Regset.empty
       end
@@ -167,6 +169,8 @@ Definition transf_instr
       Ltailcall sig (sum_left_map assign ros) (List.map assign args)
   | Icond cond args ifso ifnot =>
       Lcond cond (List.map assign args) ifso ifnot
+  | Ijumptable arg tbl =>
+      Ljumptable (assign arg) tbl
   | Ireturn optarg =>
       Lreturn (option_map assign optarg)
   end.
-- 
cgit