aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-11-06 14:38:07 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-11-06 14:38:07 +0100
commitd0049e3b6bafb3aa88e173c10183b564918de115 (patch)
tree8031e22caf06c0855f36d9b4214ed3b8ee0dbf15 /cfrontend/C2C.ml
parentd9584e32f6b6f3a44d54615c97a5998c0ba6dfd5 (diff)
downloadcompcert-d0049e3b6bafb3aa88e173c10183b564918de115.tar.gz
compcert-d0049e3b6bafb3aa88e173c10183b564918de115.zip
Fix for switch was to eager.
We should not remove any debug stmt inside of the cases. We should just not warn in the case that init is only debugcalls. Bug 17850
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml14
1 files changed, 8 insertions, 6 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 913b2874..6b3426b2 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -918,11 +918,8 @@ let rec groupSwitch = function
let (fst, cases) = groupSwitch rem in
(Cutil.sskip, (case, fst) :: cases)
| Stmt s :: rem ->
- if Cutil.is_debug_stmt s then
- groupSwitch rem
- else
- let (fst, cases) = groupSwitch rem in
- (Cutil.sseq s.sloc s fst, cases)
+ 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 =
@@ -986,7 +983,12 @@ let rec convertStmt env s =
Scontinue
| C.Sswitch(e, s1) ->
let (init, cases) = groupSwitch (flattenSwitch s1) in
- if init.sdesc <> C.Sskip then
+ let rec init_debug s =
+ match s.sdesc with
+ | Sseq (a,b) -> init_debug a && init_debug b
+ | C.Sskip -> true
+ | _ -> Cutil.is_debug_stmt s in
+ if init.sdesc <> C.Sskip && not (init_debug init) then
begin
warning "ignored code at beginning of 'switch'";
contains_case init