aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Unblock.ml
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 /cparser/Unblock.ml
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
Diffstat (limited to 'cparser/Unblock.ml')
-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 ->