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

(limited to 'backend/Linear.v')

diff --git a/backend/Linear.v b/backend/Linear.v
index e025407a..bf21cb7d 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -46,6 +46,7 @@ Inductive instruction: Type :=
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list mreg -> label -> instruction
+  | Ljumptable: mreg -> list label -> instruction
   | Lreturn: instruction.
 
 Definition code: Type := list instruction.
@@ -293,6 +294,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond (reglist rs args) = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b rs m)
+  | exec_Ljumptable:
+      forall s f sp arg tbl b rs m n lbl b',
+      rs (R arg) = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some lbl ->
+      find_label lbl f.(fn_code) = Some b' ->
+      step (State s f sp (Ljumptable arg tbl :: b) rs m)
+        E0 (State s f sp b' rs m)
   | exec_Lreturn:
       forall s f stk b rs m,
       step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m)
-- 
cgit