From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy 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 --- lib/Integers.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'lib/Integers.v') 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. -- cgit