diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-11-06 14:18:31 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-11-06 14:18:31 +0100 |
commit | d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5 (patch) | |
tree | 0dd82144fd5f95ed834b37a7db6e2c91f801c9bd /cparser/Cutil.ml | |
parent | 76cb39f790fc3bf4d1e2fae99cda7eeae8bbbbf2 (diff) | |
download | compcert-kvx-d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5.tar.gz compcert-kvx-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.
Diffstat (limited to 'cparser/Cutil.ml')
-rw-r--r-- | cparser/Cutil.ml | 16 |
1 files changed, 12 insertions, 4 deletions
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) } - - - - |