- 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

1 files changed, 5 insertions, 4 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 3bf790c..7cb604e 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]].