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

(limited to 'backend/LTL.v')

diff --git a/backend/LTL.v b/backend/LTL.v
index 2505566f..6a693361 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -42,6 +42,7 @@ Inductive instruction: Type :=
   | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction
   | Ltailcall: signature -> loc + ident -> list loc -> instruction
   | Lcond: condition -> list loc -> node -> node -> instruction
+  | Ljumptable: loc -> list node -> instruction
   | Lreturn: option loc -> instruction.
 
 Definition code: Type := PTree.t instruction.
@@ -206,6 +207,13 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond (map rs args) = Some false ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifnot rs m)
+  | exec_Ljumptable:
+      forall s f sp pc rs m arg tbl n pc',
+      (fn_code f)!pc = Some(Ljumptable arg tbl) ->
+      rs arg = Vint n ->
+      list_nth_z tbl (Int.signed n) = Some pc' ->
+      step (State s f sp pc rs m)
+        E0 (State s f sp pc' rs m)
   | exec_Lreturn:
       forall s f stk pc rs m or,
       (fn_code f)!pc = Some(Lreturn or) ->
@@ -263,6 +271,7 @@ Definition successors_instr (i: instruction) : list node :=
   | Lcall sig ros args res s => s :: nil
   | Ltailcall sig ros args => nil
   | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Ljumptable arg tbl => tbl
   | Lreturn optarg => nil
   end.
 
-- 
cgit