- 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, 7 insertions, 4 deletions

diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 51a45b2..19f4c83 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -272,12 +272,15 @@ let rec print_stmt p s =
               print_stmt s
   | Sexit n ->
       fprintf p "exit %d;" (Nat.to_int n)
-  | Sswitch(e, cases, dfl) ->
-      fprintf p "@[<v 2>switch (%a) {" print_expr e;
+  | Sswitch(long, e, cases, dfl) ->
+      fprintf p "@[<v 2>switch%s (%a) {"
+        (if long then "l" else "") print_expr e;
       List.iter
         (fun (n, x) ->
-           fprintf p "@ case %ld: exit %d;" 
-                     (camlint_of_coqint n) (Nat.to_int x))
+           fprintf p "@ case %s%s: exit %d;" 
+                     (Z.to_string n)
+                     (if long then "LL" else "")
+                     (Nat.to_int x))
         cases;
       fprintf p "@ default: exit %d;\n" (Nat.to_int dfl);
       fprintf p "@;<0 -2>}@]"