From 8492d8f3b982065bb5c22bec0a94dab8f55c7de1 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 18 Jun 2021 18:56:40 +0200
Subject: [PATCH] [typing] do not consider non-type attributes when comparing
args of TFun
only type attributes are relevant here.
---
src/kernel_services/ast_queries/cil.ml | 2 +-
src/kernel_services/ast_queries/cil_datatype.ml | 5 ++---
tests/spec/oracle/unused_parameter_attribute.res.oracle | 2 +-
3 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 3667813a8fb..23900b64093 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 539184f0204..8058a931418 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 809fe3405fb..eb4879183f5 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;
--
GitLab