aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-11-06 14:18:31 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-11-06 14:18:31 +0100
commitd9584e32f6b6f3a44d54615c97a5998c0ba6dfd5 (patch)
tree0dd82144fd5f95ed834b37a7db6e2c91f801c9bd
parent76cb39f790fc3bf4d1e2fae99cda7eeae8bbbbf2 (diff)
downloadcompcert-d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5.tar.gz
compcert-d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5.zip
Remove debug stmts during grouping of switch.
Debug statements introduced during the translation result in warnings when they are introduced at the head of the switch. Since they are not used and the warning is not necessary we can remove them before. Fix 17580.
-rw-r--r--cfrontend/C2C.ml8
-rw-r--r--cparser/Cutil.ml16
-rw-r--r--cparser/Cutil.mli2
3 files changed, 19 insertions, 7 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index a2db0915..913b2874 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -918,8 +918,11 @@ let rec groupSwitch = function
let (fst, cases) = groupSwitch rem in
(Cutil.sskip, (case, fst) :: cases)
| Stmt s :: rem ->
- let (fst, cases) = groupSwitch rem in
- (Cutil.sseq s.sloc s fst, cases)
+ if Cutil.is_debug_stmt s then
+ groupSwitch rem
+ else
+ 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 =
@@ -1313,4 +1316,3 @@ let convertProgram p =
if Cerrors.check_errors () then None else Some p'
with Env.Error msg ->
error (Env.error_message msg); None
-
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index a86c779f..1b0bf65d 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -880,6 +880,18 @@ let is_literal_0 e =
| EConst(CInt(0L, _, _)) -> true
| _ -> false
+(* Check that a C statement is a debug annotation *)
+
+let is_debug_stmt s =
+ let is_debug_call = function
+ | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug"
+ | _ -> false in
+ match s.sdesc with
+ | Sdo {edesc = e;_} ->
+ is_debug_call e
+ | _ -> false
+
+
(* Assignment compatibility check over attributes.
Standard attributes ("const", "volatile", "restrict") can safely
be added (to the rhs type to get the lhs type) but must not be dropped.
@@ -1099,7 +1111,3 @@ let rec subst_stmt phi s =
List.map subst_asm_operand inputs,
clob)
}
-
-
-
-
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 8b6c609b..b353cba3 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -187,6 +187,8 @@ val type_of_member : Env.t -> field -> typ
(* Return the type of accessing the given field [fld].
Normally it's [fld.fld_type] but there is a special case for
small unsigned bitfields. *)
+val is_debug_stmt : stmt -> bool
+ (* Is the given statement a call to debug builtin? *)
val is_literal_0 : exp -> bool
(* Is the given expression the integer literal "0"? *)
val is_lvalue : exp -> bool