From ede425855bfd5cd4c13e3a11479a5e9d05acad58 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 22 Apr 2013 11:35:32 +0000
Subject: Labeled statements inside switch were incorrectly processed.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2211 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/C2C.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'cfrontend')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 0ffbd66..e1b7705 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -618,6 +618,9 @@ let rec flattenSwitch = function
       Label(Case e) :: flattenSwitch s1
   | {sdesc = C.Slabeled(C.Sdefault, s1)} ->
       Label Default :: flattenSwitch s1
+  | {sdesc = C.Slabeled(C.Slabel lbl, s1); sloc = loc} ->
+      Stmt {sdesc = C.Slabeled(C.Slabel lbl, Cutil.sskip); sloc = loc}
+      :: flattenSwitch s1
   | s ->
       [Stmt s]
 
-- 
cgit v1.2.3