diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 6a38cc02b3662b0a9b5381992257f57b284e3153..e28a4aad94d94e8d58a2d305a80f9b3518ef8ed6 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 778b8ccd6cc2a6ed0b9c339dd6406cbc48c93226..d284cd66c6f948349613fb3d9e87e405cc1a98f5 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 0000000000000000000000000000000000000000..e2ac976c5094141a728ffa2760e13a24725641ca --- /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 0000000000000000000000000000000000000000..03dbb7f08ee8af4eae99b62f8a1e7e64c920b8e5 --- /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; +} + +