diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-10-24 15:20:21 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-10-29 10:03:30 +0200 |
| commit | dfc6b66ec21e148d29b2a6e8b5d77873a0a47511 (patch) | |
| tree | e1b35810458543758dd5929b0546d81e9db7993c | |
| parent | efc51afc7c8298ecd3b511b8d0faf9ff6d2df22e (diff) | |
| download | compcert-dfc6b66ec21e148d29b2a6e8b5d77873a0a47511.tar.gz compcert-dfc6b66ec21e148d29b2a6e8b5d77873a0a47511.zip | |
Unblock: never put debug info before a label
This ensures that normalized switch statements remain normalized.
However, if the label and the labeled statement are on different lines,
add an extra line directive corresponding to the label before the labeled
statement.
| -rw-r--r-- | cparser/Unblock.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 4b1f2262..71d800c3 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 cts ploc s1 in + {s with sdesc = Slabeled(lbl, s1')} | Sgoto lbl -> add_lineno ctx ploc s.sloc s | Sreturn None -> |