diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-17 12:05:21 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-17 12:05:21 +0000 |
| commit | 0e4def2853d5cfa9034344a5c4570543ed271ee2 (patch) | |
| tree | 7f23324f93d1fbe3f115a7fc79b809e1f7a44dc4 /cfrontend | |
| parent | 34a2dec2f1fab835aec0799f5b4758df31e688ff (diff) | |
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
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 11 |
1 files changed, 7 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 *) |