aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-07-06 12:51:42 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-07-06 12:51:42 +0200
commite30aa60a06817ed67c14a80430a7275defc41e76 (patch)
treeb4bb512416a40578db1f32eb3a7836ddb6f8582d /cfrontend/C2C.ml
parentaa780c7145a418b4a7264e828258034fc4629313 (diff)
parent2f31c1867b75040067a1ef74ae32f197e8d296c1 (diff)
downloadcompcert-kvx-e30aa60a06817ed67c14a80430a7275defc41e76.tar.gz
compcert-kvx-e30aa60a06817ed67c14a80430a7275defc41e76.zip
Merge branch 'master' into json_export
Conflicts: driver/Driver.ml
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml28
1 files changed, 27 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 71328c71..b919c1d4 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -572,6 +572,7 @@ let z_of_str hex str fst =
done;
!res
+
let checkFloatOverflow f =
match f with
| Fappli_IEEE.B754_finite _ -> ()
@@ -897,6 +898,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 +976,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