diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 742b5c26528ecaa01b59f948db601f221c025f8c..2b6bb63708b08cfd0bb5dd6d161a9f01fefc19e5 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -440,6 +440,9 @@ let attributeHash: (string, attributeClass) Hashtbl.t = [ "stdcall";"cdecl"; "fastcall"; "noreturn"]; List.iter (fun a -> Hashtbl.add table a AttrType) ("mode" :: qualifier_attributes); + (* GCC label and statement attributes. *) + List.iter (fun a -> Hashtbl.add table a AttrStmt) + [ "hot"; "cold"; "fallthrough"; "assume"; "musttail" ]; table let isKnownAttribute = Hashtbl.mem attributeHash diff --git a/tests/syntax/oracle/stmt_attributes.0.res.oracle b/tests/syntax/oracle/stmt_attributes.0.res.oracle index 504d94e316eba1f94d11ddfa357e02adff8a1a1d..734410a37054c66ae2f5b989ec53e067f78f284c 100644 --- a/tests/syntax/oracle/stmt_attributes.0.res.oracle +++ b/tests/syntax/oracle/stmt_attributes.0.res.oracle @@ -1,6 +1,4 @@ [kernel] Parsing stmt_attributes.c (with preprocessing) -[kernel:unknown-attribute] stmt_attributes.c:11: Warning: - Unknown attribute: fallthrough /* Generated by Frama-C */ void f(void) {