diff options
| -rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
| -rw-r--r-- | cparser/C.mli | 2 | ||||
| -rw-r--r-- | cparser/Cleanup.ml | 2 | ||||
| -rw-r--r-- | cparser/Cprint.ml | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 10 | ||||
| -rw-r--r-- | cparser/Rename.ml | 2 |
6 files changed, 10 insertions, 10 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e9a3ea92..5777eb96 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1005,7 +1005,7 @@ type switchbody = let rec flattenSwitch = function | {sdesc = C.Sseq(s1, s2)} -> flattenSwitch s1 @ flattenSwitch s2 - | {sdesc = C.Slabeled(C.Scase e, s1)} -> + | {sdesc = C.Slabeled(C.Scase(e, _), s1)} -> Label(Case e) :: flattenSwitch s1 | {sdesc = C.Slabeled(C.Sdefault, s1)} -> Label Default :: flattenSwitch s1 diff --git a/cparser/C.mli b/cparser/C.mli index d674afb8..cc8d4065 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -220,7 +220,7 @@ and stmt_desc = and slabel = | Slabel of string - | Scase of exp + | Scase of exp * int64 | Sdefault (** Declarations *) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index 9568d8fe..63ac8ac1 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -93,7 +93,7 @@ let rec add_stmt s = | Scontinue -> () | Sswitch(e, s1) -> add_exp e; add_stmt s1 | Slabeled(lbl, s) -> - begin match lbl with Scase e -> add_exp e | _ -> () end; + begin match lbl with Scase(e, _) -> add_exp e | _ -> () end; add_stmt s | Sgoto lbl -> () | Sreturn None -> () diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index c2253c8f..9aeec421 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -478,7 +478,7 @@ let rec stmt pp s = and slabel pp = function | Slabel s -> fprintf pp "%s" s - | Scase e -> + | Scase(e, _) -> fprintf pp "case %a" exp (0, e) | Sdefault -> fprintf pp "default" diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 0194a893..b8a4ebf6 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2585,13 +2585,13 @@ let rec elab_stmt env ctx s = if not ctx.ctx_in_switch then error loc "'case' statement not in switch statement"; let a',env = elab_expr ctx.ctx_vararg loc env a in - begin match Ceval.integer_expr env a' with + let n = + match Ceval.integer_expr env a' with | None -> - error loc "expression of 'case' label is not an integer constant expression" - | Some n -> () - end; + error loc "expression of 'case' label is not an integer constant expression"; 0L + | Some n -> n in let s1,env = elab_stmt env ctx s1 in - { sdesc = Slabeled(Scase a', s1); sloc = elab_loc loc },env + { sdesc = Slabeled(Scase(a', n), s1); sloc = elab_loc loc },env | DEFAULT(s1, loc) -> if not ctx.ctx_in_switch then diff --git a/cparser/Rename.ml b/cparser/Rename.ml index d63fa47d..eb31eaf0 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -188,7 +188,7 @@ and stmt_or_decl env s = (stmt env s, env) and slabel env = function - | Scase e -> Scase(exp env e) + | Scase(e, n) -> Scase(exp env e, n) | sl -> sl let fundef env f = |