diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-30 14:49:04 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-30 14:49:04 +0200 |
commit | d8ed56833c508b5103a900ef04975013bd9ba77b (patch) | |
tree | c6091bfd87a50a0915ce01629cc96cae1686695c /cfrontend/C2C.ml | |
parent | bdbf444704c031a37039d4aeb2f19d05550afbd6 (diff) | |
parent | 19fd986669c098333b88758e85ba146c78a281bf (diff) | |
download | compcert-d8ed56833c508b5103a900ef04975013bd9ba77b.tar.gz compcert-d8ed56833c508b5103a900ef04975013bd9ba77b.zip |
Merge branch 'master' of https://github.com/AbsInt/CompCert
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r-- | cfrontend/C2C.ml | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 71328c71..96a497bc 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -897,6 +897,28 @@ let rec groupSwitch = function 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 = + match s.sdesc with + | C.Sskip + | C.Sdo _ + | C.Sbreak + | C.Scontinue + | C.Sswitch _ (* Stop at a switch *) + | C.Sgoto _ + | C.Sreturn _ + | C.Sdecl _ + | C.Sasm _ -> () + | C.Sseq (s1,s2) + | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 + | C.Swhile (_,s1) + | C.Sdowhile (s1,_) -> contains_case s1 + | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 + | C.Slabeled(C.Scase _, _) -> + unsupported "'case' outside of 'switch'" + | C.Slabeled(_,s) -> contains_case s + | C.Sblock b -> List.iter contains_case b + (** Annotations for line numbers *) let add_lineno prev_loc this_loc s = @@ -953,7 +975,10 @@ let rec convertStmt ploc env s = | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in if init.sdesc <> C.Sskip then - warning "ignored code at beginning of 'switch'"; + begin + warning "ignored code at beginning of 'switch'"; + contains_case init + end; let te = convertExpr env e in add_lineno ploc s.sloc (swrap (Ctyping.sswitch te |