Index: src/cil.ml
===================================================================
--- src/cil.ml	(revision 12120)
+++ src/cil.ml	(working copy)
@@ -6486,6 +6486,9 @@
   switch_count := 1 + !switch_count ;
   !switch_count
 
+exception Default_present of location
+(* Used to signal that a [Default] label has been found *)
+
 let rec xform_switch_stmt s break_dest cont_dest label_index = begin
   s.labels <- Util.list_map (fun lab -> match lab with
     Label _ -> lab
@@ -6522,7 +6525,7 @@
                 end
   | If(e,b1,b2,l) -> xform_switch_block b1 break_dest cont_dest label_index ;
                      xform_switch_block b2 break_dest cont_dest label_index
-  | Switch(e,b,sl,l) -> begin
+  | Switch(se,body,sl,l) -> begin
       (* change 
        * switch (se) {
        *   case 0: s0 ;
@@ -6533,59 +6536,102 @@
        * into:
        *
        * if (se == 0) goto label_0;
-       * else if (se == 1) goto label_1;
+       * if (se == 1) goto label_1;
        * ...
-       * else if (0) { // body_block
-       *  label_0: s0;
-       *  label_1: s1; goto label_break;
-       *  ...
-       * } else if (0) { // break_block
-       *  label_break: ; // break_stmt
-       * } 
+       * goto label_default; // If there is a [Default]
+       * goto label_break; // If there is no [Default]; this prevents falling through into the switch's body
+       * label_0: s0;
+       * label_1: s1; goto label_break;
+       * ...
+       * label_break: ; // break_stmt
+       * 
+       * The default case, if present, must be used only if *all*
+       * non-default cases fail [ISO/IEC 9899:1999, §6.8.4.2, ¶5]. As
+       * a result, we test all cases first, and hit 'default' only if
+       * no case matches. However, we do not reorder the switch's
+       * body, so fall-through still works as expected.
        *)
       let i = get_switch_count () in 
       let break_stmt = mkStmt (Instr []) in
       break_stmt.labels <- 
 				[Label(freshLabel (Printf.sprintf "switch_%d_break" i),l,false)] ;
-      let break_block = mkBlock [ break_stmt ] in
-      let body_block = b in 
-      let body_if_stmtkind = (If(zero,body_block,break_block,l)) in
 
-      (* The default case, if present, must be used only if *all*
-      non-default cases fail [ISO/IEC 9899:1999, §6.8.4.2, ¶5]. As a
-      result, we sort the order in which we handle the labels (but not the
-      order in which we print out the statements, so fall-through still
-      works as expected). *)
-      let compare_choices s1 s2 = match s1.labels, s2.labels with
-      | (Default(_) :: _), _ -> 1
-      | _, (Default(_) :: _) -> -1
-      | _, _ -> 0
+      (* Put the break label at the end of the body *)
+      body.bstmts <- body.bstmts @ [break_stmt];
+
+      (* Returns a list of triples of the form (x==i, stmt, loc) for one
+         section of switch statement. For example,
+           case 0:
+           case 5:
+           case 1: s;
+         becomes [(se==0, s, 0); (se==5, s, 1); (se==1, s, 2)].
+         [Label]s are ignored. If a [Default] is encountered, a
+         [Default_present] exception is raised. *)
+      let get_eqs_stmts_locs stmt : (exp * stmt * location) list =
+          List.fold_left
+              (fun result label -> match label with
+                     Case (exp, loc) -> (BinOp(Eq,se,exp,intType), stmt, loc) :: result
+                   | Label _ -> result
+                   | Default loc -> raise (Default_present loc))
+              []
+              stmt.labels
       in
 
-      let rec handle_choices sl = match sl with
-        [] -> body_if_stmtkind
-      | stmt_hd :: stmt_tl -> begin
-        let rec handle_labels lab_list = begin
-          match lab_list with
-            [] -> handle_choices stmt_tl 
-          | Case(ce,cl) :: lab_tl -> 
-              let pred = BinOp(Eq,e,ce,intType) in
-              let then_block = mkBlock [ mkStmt (Goto(ref stmt_hd,cl)) ] in
-              let else_block = mkBlock [ mkStmt (handle_labels lab_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) ])
-          | Label(_,_,_) :: lab_tl -> handle_labels lab_tl
-        end in
-        handle_labels stmt_hd.labels
-      end in
-      s.skind <- handle_choices (List.sort compare_choices sl) ;
-      xform_switch_block b (fun () -> ref break_stmt) cont_dest i 
+      (* Get a list of lists of (eq, stmt, loc) triples.
+         Also, get the stmt and loc for the goto statement that will
+         sit between the conditions and the switch body. If there is a
+         [Default], it will go to the corresponding statement;
+         otherwise, it will go to break_stmt. *)
+      let (all_eqs_stmts_locs : (exp * stmt * location) list list), default_target, default_loc =
+          List.fold_left
+              (fun (all_eqs_stmts_locs, default_target, default_loc) stmt ->
+                   try
+                       let eqs_stmts_locs = get_eqs_stmts_locs stmt in
+                       (eqs_stmts_locs :: all_eqs_stmts_locs, default_target, default_loc)
+                   with Default_present loc ->
+                       (all_eqs_stmts_locs, stmt, loc))
+              ([], break_stmt, l) (* Use the switch statement's location for this goto. *)
+              sl
+      in
+
+      (* Put the default_goto before the switch body. *)
+      body.bstmts <- mkStmt (Goto (ref default_target, default_loc)) :: body.bstmts;
+
+      (* Convert all_eqs_and_gotos into a single list. If we can use
+         '||', each list gets converted into a single disjunction:
+           ((se==0 || se==1 || ... || se==n), goto stmt)
+         Otherwise, we just flatten the list of lists, so each 'se==i'
+         stands alone: (se==i, goto stmt). *)
+      let preds_stmts_locs =
+          if !useLogicalOperators
+          then (
+              let make_disjunction = function
+                    [] -> E.s (bug "Expected at least one Case label")
+                  | (eq, stmt, loc) :: eqs_stmts_locs ->
+                        let disjunction =
+                            List.fold_left
+                                (fun eqs (eq, _, _) -> BinOp(LOr, eq, eqs, intType))
+                                eq
+                                eqs_stmts_locs
+                        in (disjunction, stmt, loc) (* Use the stmt and loc of the first equality check *)
+              in
+              List.map make_disjunction all_eqs_stmts_locs
+          ) else List.flatten all_eqs_stmts_locs
+      in
+      (* Prepend all 'if' checks to the body *)
+      List.iter
+          (fun (pred, stmt, loc) ->
+               let goto = mkStmt (Goto (ref stmt, loc)) in
+               body.bstmts <-
+                   mkStmt (If (pred, mkBlock [ goto ], mkBlock [], loc)) ::
+                   body.bstmts)
+          preds_stmts_locs;
+
+      (* Replace s's stmtkind with the block we've constructed *)
+      s.skind <- Block body;
+
+      (* Now transform the body, making any 'break;' statements jump to break_stmt *)
+      xform_switch_block body (fun () -> ref break_stmt) cont_dest i 
     end
   | Loop(b,l,_,_) -> 
           let i = get_switch_count () in