aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-11-06 14:18:31 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-11-06 14:18:31 +0100
commitd9584e32f6b6f3a44d54615c97a5998c0ba6dfd5 (patch)
tree0dd82144fd5f95ed834b37a7db6e2c91f801c9bd /cfrontend/C2C.ml
parent76cb39f790fc3bf4d1e2fae99cda7eeae8bbbbf2 (diff)
downloadcompcert-d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5.tar.gz
compcert-d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5.zip
Remove debug stmts during grouping of switch.
Debug statements introduced during the translation result in warnings when they are introduced at the head of the switch. Since they are not used and the warning is not necessary we can remove them before. Fix 17580.
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index a2db0915..913b2874 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -918,8 +918,11 @@ let rec groupSwitch = function
let (fst, cases) = groupSwitch rem in
(Cutil.sskip, (case, fst) :: cases)
| Stmt s :: rem ->
- let (fst, cases) = groupSwitch rem in
- (Cutil.sseq s.sloc s fst, cases)
+ if Cutil.is_debug_stmt s then
+ groupSwitch rem
+ else
+ let (fst, cases) = groupSwitch rem in
+ (Cutil.sseq s.sloc s fst, cases)
(* Test whether the statement contains case and give an *)
let rec contains_case s =
@@ -1313,4 +1316,3 @@ let convertProgram p =
if Cerrors.check_errors () then None else Some p'
with Env.Error msg ->
error (Env.error_message msg); None
-