diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-17 07:52:12 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-17 07:52:12 +0000 |
commit | 17f519651feb4a09aa90c89c949469e8a5ab0e88 (patch) | |
tree | c7bda5e43a2d1f950180521a1b854ac9592eea73 /cfrontend/Cminorgenproof.v | |
parent | 88613c0f5415a0d3f2e0e0e9ff74bd32b6b4685e (diff) | |
download | compcert-17f519651feb4a09aa90c89c949469e8a5ab0e88.tar.gz compcert-17f519651feb4a09aa90c89c949469e8a5ab0e88.zip |
- 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
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
-rw-r--r-- | cfrontend/Cminorgenproof.v | 9 |
1 files changed, 5 insertions, 4 deletions
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]]. |