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

1 files changed, 25 insertions, 0 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 1eb59c5c..c54b6fe5 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -657,6 +657,13 @@ Proof.
   apply eqm_samerepr. unfold z'; red. exists 1. omega.
 Qed.
 
+Theorem signed_eq_unsigned:
+  forall x, unsigned x <= max_signed -> signed x = unsigned x.
+Proof.
+  intros. unfold signed. destruct (zlt (unsigned x) half_modulus).
+  auto. unfold max_signed in H. omegaContradiction.
+Qed.
+
 (** ** Properties of addition *)
 
 Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y).
@@ -786,6 +793,13 @@ Proof.
   symmetry. apply sub_add_opp.
 Qed.
 
+Theorem sub_signed:
+  forall x y, sub x y = repr (signed x - signed y).
+Proof.
+  intros. unfold sub. apply eqm_samerepr.
+  apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned.
+Qed.
+
 (** ** Properties of multiplication *)
 
 Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -2565,4 +2579,15 @@ Proof.
   omega. 
 Qed.
 
+Theorem ltu_range_test:
+  forall x y,
+  ltu x y = true -> unsigned y <= max_signed ->
+  0 <= signed x < unsigned y.
+Proof.
+  intros.
+  unfold Int.ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate.
+  rewrite signed_eq_unsigned.
+  generalize (unsigned_range x). omega. omega.
+Qed.
+
 End Int.