From b1dbe72eacb731f193ac475ac1d14a20a832b8aa Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 23 Apr 2018 11:25:03 +0200
Subject: Detect duplicate 'case' or 'default' statements within a 'switch'

Report an error in this case.
---
 cparser/Elab.ml | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

(limited to 'cparser/Elab.ml')

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 *)
-- 
cgit