aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-03-21 15:46:43 +0100
committerBernhard Schommer <bschommer@users.noreply.github.com>2017-03-24 11:59:58 +0100
commitb6b5aae1d406c200035ff7400de46eed2d88fd85 (patch)
tree8990b00fcf497fb35aadc7631b2fe94f225410c5
parent8827f9bc5d68726bc04a4cd8d26321868bd76b7f (diff)
downloadcompcert-kvx-b6b5aae1d406c200035ff7400de46eed2d88fd85.tar.gz
compcert-kvx-b6b5aae1d406c200035ff7400de46eed2d88fd85.zip
Do not emit line info before case stmt.
Since before a case statement is potentially unreachable code due to break, etc. it is better to skip printing line information directly before the case statement and print it afterwards. Bug 21232
-rw-r--r--cparser/Unblock.ml13
1 files changed, 9 insertions, 4 deletions
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 87b2f9bb..ad68afbc 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -215,10 +215,10 @@ let debug_scope ctx =
Add scope debug annotation regardless. *)
-let add_lineno ctx prev_loc this_loc s =
+let add_lineno ?(case=false) 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
+ (if this_loc <> prev_loc && this_loc <> no_loc && not case
then sseq no_loc (debug_lineno this_loc) s
else s)
else s
@@ -254,6 +254,10 @@ let process_decl loc env ctx (sto, id, ty, optinit) k =
let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in
add_inits_stmt loc l k
+let is_case = function
+ | Slabel _ -> false
+ | _ -> true
+
(* Simplification of blocks within a statement *)
let rec unblock_stmt env ctx ploc s =
@@ -291,8 +295,9 @@ 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) ->
- add_lineno ctx ploc s.sloc
- {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
+ let loc,case = if is_case lbl then ploc,true else s.sloc,false in
+ add_lineno ~case:case ctx ploc s.sloc
+ {s with sdesc = Slabeled(lbl, unblock_stmt env ctx loc s1)}
| Sgoto lbl ->
add_lineno ctx ploc s.sloc s
| Sreturn None ->