From 69295f84a93e773003b4bd7325461d57d990d90b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 23 Jan 2024 15:08:48 +0100
Subject: [PATCH] [Cil] avoid crashing due to attribute differences

Attributes such as 'visibility' must be ignored for casting purposes,
to avoid errors with implicit casts.
---
 src/kernel_services/ast_queries/cil.ml               | 12 ++++++++++--
 tests/syntax/cast-struct-function-attr.i             |  7 +++++++
 .../oracle/cast-struct-function-attr.res.oracle      |  1 +
 .../syntax/oracle/cast-struct-function-attr_ocode.i  | 12 ++++++++++++
 4 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 tests/syntax/oracle/cast-struct-function-attr.res.oracle
 create mode 100644 tests/syntax/oracle/cast-struct-function-attr_ocode.i

diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6a38cc02b36..e28a4aad94d 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -401,6 +401,8 @@ let qualifier_attributes = [ "const"; "restrict"; "volatile"; "ghost" ]
 
 let fc_internal_attributes = ["declspec"; "arraylen"; "fc_stdlib"]
 
+let cast_irrelevant_attributes = ["visibility"]
+
 let filter_qualifier_attributes al =
   List.filter
     (fun a -> List.mem (attributeName a) qualifier_attributes) al
@@ -5020,14 +5022,20 @@ let spare_attributes_for_c_cast =
   fc_internal_attributes @ qualifier_attributes
 
 let type_remove_attributes_for_c_cast t =
-  let t = typeRemoveAttributesDeep fc_internal_attributes t in
+  let attributes_to_remove =
+    fc_internal_attributes @ cast_irrelevant_attributes
+  in
+  let t = typeRemoveAttributesDeep attributes_to_remove t in
   typeRemoveAttributes spare_attributes_for_c_cast t
 
 let spare_attributes_for_logic_cast =
   spare_attributes_for_c_cast
 
 let type_remove_attributes_for_logic_type t =
-  let t = typeRemoveAttributesDeep fc_internal_attributes t in
+  let attributes_to_remove =
+    fc_internal_attributes @ cast_irrelevant_attributes
+  in
+  let t = typeRemoveAttributesDeep attributes_to_remove t in
   typeRemoveAttributes spare_attributes_for_logic_cast t
 
 let () = Cil_datatype.drop_non_logic_attributes :=
diff --git a/tests/syntax/cast-struct-function-attr.i b/tests/syntax/cast-struct-function-attr.i
index 778b8ccd6cc..d284cd66c6f 100644
--- a/tests/syntax/cast-struct-function-attr.i
+++ b/tests/syntax/cast-struct-function-attr.i
@@ -1,3 +1,10 @@
+/* run.config*
+  LOG: @PTEST_NAME@_ocode.i
+  STDOPT: -print -ocode @PTEST_NAME@_ocode.i
+ENABLED_IF: %{bin-available:gcc}
+  EXECNOW: LOG @PTEST_NAME@.out LOG @PTEST_NAME@.err gcc %{dep:@PTEST_NAME@_ocode.i} -c -o @DEV_NULL@ > @PTEST_NAME@.out 2> @PTEST_NAME@.err
+*/
+
 struct t {
   int a;
 };
diff --git a/tests/syntax/oracle/cast-struct-function-attr.res.oracle b/tests/syntax/oracle/cast-struct-function-attr.res.oracle
new file mode 100644
index 00000000000..e2ac976c509
--- /dev/null
+++ b/tests/syntax/oracle/cast-struct-function-attr.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing cast-struct-function-attr.i (no preprocessing)
diff --git a/tests/syntax/oracle/cast-struct-function-attr_ocode.i b/tests/syntax/oracle/cast-struct-function-attr_ocode.i
new file mode 100644
index 00000000000..03dbb7f08ee
--- /dev/null
+++ b/tests/syntax/oracle/cast-struct-function-attr_ocode.i
@@ -0,0 +1,12 @@
+/* Generated by Frama-C */
+struct t {
+   int a ;
+};
+typedef struct t t;
+t __attribute__((__visibility__("hidden"))) f(void)
+{
+  t res = {.a = 0};
+  return res;
+}
+
+
-- 
GitLab