From 95feb01fea4eef86244f15cef31216be3670262a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 5 Nov 2024 10:46:30 +0100
Subject: [PATCH] [cil] Register GCC Label and Statement attribute
For now we ignore "unused" label attribute, because the current mecanism
does not support different attributes with the same name : "unused" can
be a label attribute or a function attribute.
---
src/kernel_services/ast_queries/cil.ml | 3 +++
tests/syntax/oracle/stmt_attributes.0.res.oracle | 2 --
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 742b5c2652..2b6bb63708 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 504d94e316..734410a370 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)
{
--
GitLab