From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Aug 2014 07:52:12 +0000 Subject: - 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 --- backend/CMtypecheck.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/CMtypecheck.ml') diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 02c3f21..aacbf86 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -313,8 +313,8 @@ let rec type_stmt env blk ret s = | Sexit n -> if Nat.to_int n >= blk then raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n))) - | Sswitch(e, cases, deflt) -> - unify (type_expr env [] e) tint + | Sswitch(islong, e, cases, deflt) -> + unify (type_expr env [] e) (if islong then tlong else tint) | Sreturn None -> begin match ret with | None -> () -- cgit v1.2.3