diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-07 16:06:33 +0100 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-07 16:06:33 +0100 |
| commit | 99761d109a799f6ca62471058463b5713f37eddc (patch) | |
| tree | f8038305ef9596629eb6084ff64044451fac1656 /cparser/Cutil.ml | |
| parent | 15e6fc9861641d03ac32ae9ac03b9a6fa68036e9 (diff) | |
| parent | d0049e3b6bafb3aa88e173c10183b564918de115 (diff) | |
| download | compcert-99761d109a799f6ca62471058463b5713f37eddc.tar.gz compcert-99761d109a799f6ca62471058463b5713f37eddc.zip | |
Merge remote-tracking branch 'origin/master' into parser_fix
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) } - - - - |