From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Aug 2014 07:52:12 +0000 Subject: - Support "switch" statements over 64-bit integers (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 3bf790ca..7cb604ec 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1697,15 +1697,15 @@ Proof. - auto. - destruct (switch_table sl (S base)) as [tbl1 dfl1] eqn:ST. destruct o; simpl. - rewrite Int.eq_sym. destruct (Int.eq i i0). + rewrite dec_eq_sym. destruct (zeq i z). exists O; split; auto. constructor. specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. destruct (select_switch_case i sl). - destruct IHsl as (n & P & Q). exists (S n); split. constructor; auto. omega. + destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. auto. specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. destruct (select_switch_case i sl). - destruct IHsl as (n & P & Q). exists (S n); split. constructor; auto. omega. + destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. auto. Qed. @@ -2107,7 +2107,8 @@ Opaque PTree.set. (* switch *) simpl in TR. destruct (switch_table cases O) as [tbl dfl] eqn:STBL. monadInv TR. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. - inv VINJ. + assert (SA: switch_argument islong tv n). + { inv H0; inv VINJ; constructor. } exploit switch_descent; eauto. intros [k1 [A B]]. exploit switch_ascent; eauto. eapply (switch_table_select n). rewrite STBL; simpl. intros [k2 [C D]]. -- cgit