diff options
Diffstat (limited to 'cparser')
-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 |
5 files changed, 9 insertions, 9 deletions
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 = |