From 0e4def2853d5cfa9034344a5c4570543ed271ee2 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Aug 2014 12:05:21 +0000
Subject: 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
---
 common/Switchaux.ml | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

(limited to 'common')

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
+**)
-- 
cgit v1.2.3