diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 3667813a8fb107fef01c5fbb8622c597d12e7989..23900b640933ece2d12960901d2e8f5bce7b1697 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -4951,7 +4951,7 @@ let mk_behavior ?(name=default_behavior_name) ?(assumes=[]) ?(requires=[]) } let spare_attributes_for_c_cast = - "unused"::"declspec"::"arraylen"::"fc_stdlib"::qualifier_attributes + "declspec"::"arraylen"::"fc_stdlib"::qualifier_attributes let type_remove_attributes_for_c_cast = typeRemoveAttributes spare_attributes_for_c_cast diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml index 539184f0204551c371fafc3292e6e754666cf95e..8058a9314181b5dd8af3cb317981b5d0b9b4a39b 100644 --- a/src/kernel_services/ast_queries/cil_datatype.ml +++ b/src/kernel_services/ast_queries/cil_datatype.ml @@ -555,9 +555,8 @@ and compare_type config t1 t2 = and compare_arg_list config l1 l2 = Option.compare (compare_list - (fun (_n1, t1, l1) (_n2, t2, l2) -> - (compare_chain (compare_type config) t1 t2 - (compare_attributes config)) l1 l2 + (fun (_n1, t1, _l1) (_n2, t2, _l2) -> + compare_type config t1 t2 )) l1 l2 let hash_attribute _config = function diff --git a/tests/spec/oracle/unused_parameter_attribute.res.oracle b/tests/spec/oracle/unused_parameter_attribute.res.oracle index 809fe3405fb8cc684a82625d3647c12c24f7210e..eb4879183f52163896d506fb1d7766ecc744abe0 100644 --- a/tests/spec/oracle/unused_parameter_attribute.res.oracle +++ b/tests/spec/oracle/unused_parameter_attribute.res.oracle @@ -5,7 +5,7 @@ void f(int a __attribute__((__unused__))); int main(void) { int __retres; - void (*op)(int ) = (void (*)(int ))(& f); + void (*op)(int ) = & f; /*@ assert op ≡ &f; */ ; __retres = 0; return __retres;