diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-04-23 11:25:03 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-04-27 13:54:38 +0200 |
commit | b1dbe72eacb731f193ac475ac1d14a20a832b8aa (patch) | |
tree | 865ec8a82f48a733e9f248fc27559f66ab62f709 /cparser/Elab.ml | |
parent | 6f5eec9f5f1ad4567186172a4519e598af801b94 (diff) | |
download | compcert-b1dbe72eacb731f193ac475ac1d14a20a832b8aa.tar.gz compcert-b1dbe72eacb731f193ac475ac1d14a20a832b8aa.zip |
Detect duplicate 'case' or 'default' statements within a 'switch'
Report an error in this case.
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r-- | cparser/Elab.ml | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index b8a4ebf6..219326c9 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2563,6 +2563,46 @@ let ctx_loop ctx = { ctx with ctx_break = true; ctx_continue = true } let ctx_switch ctx = { ctx with ctx_break = true; ctx_in_switch = true } +(* Check the uniqueness of 'case' and 'default' in a 'switch' *) + +module Int64Set = Set.Make(Int64) + +let check_switch_cases switch_body = + let cases = ref Int64Set.empty + and default = ref false in + let rec check s = + match s.sdesc with + | Sskip -> () + | Sdo _ -> () + | Sseq(s1, s2) -> check s1; check s2 + | Sif(_, s1, s2) -> check s1; check s2 + | Swhile(_, s1) -> check s1 + | Sdowhile(s1, _) -> check s1 + | Sfor(s1, _, s2, s3) -> check s1; check s2; check s3 + | Sbreak -> () + | Scontinue -> () + | Sswitch(_, _) -> () (* already checked during elaboration of this switch *) + | Slabeled(lbl, s1) -> + begin match lbl with + | Slabel _ -> () + | Scase(_, n) -> + if Int64Set.mem n !cases then + Diagnostics.error s.sloc "duplicate case value '%Ld'" n + else + cases := Int64Set.add n !cases + | Sdefault -> + if !default then + Diagnostics.error s.sloc "multiple default labels in one switch" + else + default := true + end + | Sgoto _ -> () + | Sreturn _ -> () + | Sblock sl -> List.iter check sl + | Sdecl _ -> () + | Sasm _ -> () + in check switch_body + (* Elaboration of statements *) let rec elab_stmt env ctx s = @@ -2673,6 +2713,7 @@ let rec elab_stmt env ctx s = error loc "controlling expression of 'switch' does not have integer type (%a invalid)" (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_switch ctx) s1 in + check_switch_cases s1'; { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env (* 6.8.6 Break and continue statements *) |