Index: src/cil.ml
===================================================================
--- src/cil.ml	(revision 12099)
+++ src/cil.ml	(working copy)
@@ -6567,19 +6570,27 @@
       | stmt_hd :: stmt_tl -> begin
         let rec handle_labels lab_list = begin
           match lab_list with
-            [] -> handle_choices stmt_tl 
+            [] -> E.s (bug "Block missing 'case' and 'default' in switch statement")
           | Case(ce,cl) :: lab_tl -> 
-              let pred = BinOp(Eq,e,ce,intType) in
+              let make_or_from_cases labels =
+                  List.fold_left
+                      (fun pred label -> match label with
+                             Case (exp, _) -> BinOp(LOr, pred, BinOp(Eq,e,exp,intType), intType)
+                           | _ -> E.s (bug "Non-'case' label after 'case' label"))
+                      (BinOp(Eq,e,ce,intType))
+                      labels
+              in
+              let pred = make_or_from_cases lab_tl in
               let then_block = mkBlock [ mkStmt (Goto(ref stmt_hd,cl)) ] in
-              let else_block = mkBlock [ mkStmt (handle_labels lab_tl) ] in
+              let else_block = mkBlock [ mkStmt (handle_choices stmt_tl) ] in
               If(pred,then_block,else_block,cl)
           | Default(dl) :: lab_tl -> 
               (* ww: before this was 'if (1) goto label', but as Ben points
               out this might confuse someone down the line who doesn't have
               special handling for if(1) into thinking that there are two
               paths here. The simpler 'goto label' is what we want. *) 
-              Block(mkBlock [ mkStmt (Goto(ref stmt_hd,dl)) ;
-                              mkStmt (handle_labels lab_tl) ])
+              body_block.bstmts <- mkStmt (Goto(ref stmt_hd,dl)) :: body_block.bstmts @ [ break_stmt ] ;
+              Block body_block
           | Label(_,_,_) :: lab_tl -> handle_labels lab_tl
         end in
         handle_labels stmt_hd.labels