aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-01-06 15:16:13 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-01-06 15:16:13 +0100
commit05f1cccccad587234c526225aa04aff041490051 (patch)
tree3e9bc441be0a5b9bdccadb09912e63f9e06af218 /cfrontend/C2C.ml
parent1278e187ddc2aa3623002b1af2dc402eb735eb16 (diff)
downloadcompcert-05f1cccccad587234c526225aa04aff041490051.tar.gz
compcert-05f1cccccad587234c526225aa04aff041490051.zip
PR#19: there is no reason to reject an empty "switch" statement.
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f9501439..118b6d2d 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -875,8 +875,6 @@ let rec convertStmt ploc env s =
Scontinue
| C.Sswitch(e, s1) ->
let (init, cases) = groupSwitch (flattenSwitch s1) in
- if cases = [] then
- unsupported "ill-formed 'switch' statement";
if init.sdesc <> C.Sskip then
warning "ignored code at beginning of 'switch'";
let te = convertExpr env e in