aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintCminor.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-10-13 11:59:45 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2017-10-13 11:59:45 +0200
commit115825af0f765bf26270f9b9a2c550eddd76d7bd (patch)
tree11b6a254e88d0d03500a24e736bb25adb04a312c /backend/PrintCminor.ml
parentb57ffbab2e5369360e29fa0cc9a6f35393ca7ca4 (diff)
downloadcompcert-kvx-115825af0f765bf26270f9b9a2c550eddd76d7bd.tar.gz
compcert-kvx-115825af0f765bf26270f9b9a2c550eddd76d7bd.zip
Distinguish between long and int for cases.
Diffstat (limited to 'backend/PrintCminor.ml')
-rw-r--r--backend/PrintCminor.ml14
1 files changed, 7 insertions, 7 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index d50e07a3..c5418d9d 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -272,15 +272,15 @@ let rec print_stmt p s =
| Sexit n ->
fprintf p "exit %d;" (Nat.to_int n)
| Sswitch(long, e, cases, dfl) ->
+ let print_case (n,x) =
+ let x = Nat.to_int x in
+ if long then
+ fprintf p "@ case %LdLL: exit %d;" (Z.to_int64 n) x
+ else
+ fprintf p "@ case %ld: exit %d;" (Z.to_int32 n) x in
fprintf p "@[<v 2>switch%s (%a) {"
(if long then "l" else "") print_expr e;
- List.iter
- (fun (n, x) ->
- fprintf p "@ case %s%s: exit %d;"
- (Z.to_string n)
- (if long then "LL" else "")
- (Nat.to_int x))
- cases;
+ List.iter print_case cases;
fprintf p "@ default: exit %d;\n" (Nat.to_int dfl);
fprintf p "@;<0 -2>}@]"
| Sreturn None ->