Issue with switch labels that are negative 32-bit integers.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 42 insertions, 4 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 702fcf2..b8586e0 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -771,7 +771,8 @@ let rec convertStmt ploc env s =
       if init.sdesc <> C.Sskip then
         warning "ignored code at beginning of 'switch'";
       let te = convertExpr env e in
-      add_lineno ploc s.sloc (Sswitch(te, convertSwitch s.sloc env cases))
+      add_lineno ploc s.sloc
+        (Sswitch(te, convertSwitch s.sloc env (is_longlong env e.etyp) cases))
   | C.Slabeled(C.Slabel lbl, s1) ->
       add_lineno ploc s.sloc
         (Slabel(intern_string lbl, convertStmt s.sloc env s1))
@@ -795,7 +796,7 @@ let rec convertStmt ploc env s =
       add_lineno ploc s.sloc
         (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid)))
 
-and convertSwitch ploc env = function
+and convertSwitch ploc env is_64 = function
   | [] ->
       LSnil
   | (lbl, s) :: rem ->
@@ -808,9 +809,11 @@ and convertSwitch ploc env = function
             match Ceval.integer_expr env e with
             | None -> unsupported "'case' label is not a compile-time integer";
                       None
-            | Some v -> Some (Z.of_uint64 v)
+            | Some v -> Some (if is_64
+                              then Z.of_uint64 v
+                              else Z.of_uint32 (Int64.to_int32 v))
       in
-      LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env rem)
+      LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem)
 
 (** Function definitions *)
 
diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 15480ae..39b484c 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -96,4 +96,39 @@ let compile_switch modulus default table =
     else compile_switch_as_tree modulus default tbl
   end
 
+(* For debugging *)
+(**
+open Format
 
+let print_table p (tbl, dfl) =
+  fprintf p "@[<v 0>";
+  List.iter
+    (fun (key, act) -> fprintf p "%s -> %d@ " (Z.to_string key) (Nat.to_int act))
+    tbl;
+  fprintf p "_ -> %d@]" (Nat.to_int dfl)
+
+let rec print_jumptable p = function
+  | [] -> fprintf p "<empty>"
+  | [n] -> fprintf p "%d" (Nat.to_int n)
+  | n::ns -> fprintf p "%d %a" (Nat.to_int n) print_jumptable ns
+
+let rec print_tree p = function
+  | CTaction n -> fprintf p "action %d" (Nat.to_int n)
+  | CTifeq(key, act, t) ->
+      fprintf p "@[<v 2>if (x == %s)@ action %d@;<0 -2>else@ %a@]"
+              (Z.to_string key) (Nat.to_int act) print_tree t
+  | CTiflt(key, t1, t2) ->
+      fprintf p "@[<v 2>if (x <u %s)@ %a@;<0 -2>else@ %a@]"
+              (Z.to_string key) print_tree t1 print_tree t2
+  | CTjumptable(ofs, sz, acts,t) ->
+      fprintf p "@[<v 2>if (x - %s <u %s)@ jumptable %a@;<0 -2>else@ %a@]"
+              (Z.to_string ofs) (Z.to_string sz)
+              print_jumptable acts print_tree t
+
+let compile_switch modulus default table =
+  let t = compile_switch modulus default table in
+  printf "@[<v 0>-------------@ ";
+  printf "Initial problem:@ %a@ " print_table (table, default);
+  printf "Decision tree:@ %a@ @]@." print_tree t;
+  t
+**)