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.mli | |
| 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.mli')
| -rw-r--r-- | cparser/Cutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |