Merge pull request #459 from AbsInt/full-switch

Handle Duff's device and other unstructured `switch` statements

1 files changed, 12 insertions, 11 deletions

diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 4b1f2262..32e09399 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -215,14 +215,12 @@ let debug_scope ctx =
   debug_annot 6L (empty_string :: List.rev_map integer_const ctx)
 
 (* Add line number debug annotation if the line number changes.
-   Labels are ignored since the code before the label can become
-   unreachable. Add scope debug annotation regardless. *)
+   Add scope debug annotation regardless. *)
 
-
-let add_lineno ?(label=false) ctx prev_loc this_loc s =
+let add_lineno ctx prev_loc this_loc s =
   if !Clflags.option_g then
     sseq no_loc (debug_scope ctx)
-      (if this_loc <> prev_loc && this_loc <> no_loc && not label
+      (if this_loc <> prev_loc && this_loc <> no_loc
        then sseq no_loc (debug_lineno this_loc) s
        else s)
   else s
@@ -295,12 +293,15 @@ let rec unblock_stmt env ctx ploc s =
         {s with sdesc = Sswitch(expand_expr true env e,
                                 unblock_stmt env ctx s.sloc s1)}
   | Slabeled(lbl, s1) ->
-    let loc,label = if s.sloc <> s1.sloc then
-        s.sloc,false (* Label and code are on different lines *)
-      else
-        ploc,true in
-    add_lineno ~label:label ctx ploc s.sloc
-        {s with sdesc = Slabeled(lbl, unblock_stmt env ctx loc s1)}
+      (* Do not put debug info before label, only after. *)
+      (* If the label and the statement are on different lines,
+         put extra debug info before s1, referring to the line of the label. *)
+      let s1' =
+        if s.sloc <> s1.sloc then
+          add_lineno ctx ploc s.sloc (unblock_stmt env ctx s.sloc s1)
+        else
+          unblock_stmt env ctx ploc s1 in
+      {s with sdesc = Slabeled(lbl, s1')}
   | Sgoto lbl ->
       add_lineno ctx ploc s.sloc s
   | Sreturn None ->