From be117601742a440be2dea89ac1cf5e264d0899c0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 17 Jun 2021 16:18:42 +0200
Subject: [PATCH] [kernel] Ignore 'unused' param attribute when casting
---
src/kernel_services/ast_queries/cil.ml | 2 +-
.../oracle/unused_parameter_attribute.res.oracle | 14 ++++++++++++++
tests/spec/unused_parameter_attribute.i | 6 ++++++
3 files changed, 21 insertions(+), 1 deletion(-)
create mode 100644 tests/spec/oracle/unused_parameter_attribute.res.oracle
create mode 100644 tests/spec/unused_parameter_attribute.i
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 23900b64093..3667813a8fb 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 =
- "declspec"::"arraylen"::"fc_stdlib"::qualifier_attributes
+ "unused"::"declspec"::"arraylen"::"fc_stdlib"::qualifier_attributes
let type_remove_attributes_for_c_cast =
typeRemoveAttributes spare_attributes_for_c_cast
diff --git a/tests/spec/oracle/unused_parameter_attribute.res.oracle b/tests/spec/oracle/unused_parameter_attribute.res.oracle
new file mode 100644
index 00000000000..809fe3405fb
--- /dev/null
+++ b/tests/spec/oracle/unused_parameter_attribute.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/spec/unused_parameter_attribute.i (no preprocessing)
+/* Generated by Frama-C */
+void f(int a __attribute__((__unused__)));
+
+int main(void)
+{
+ int __retres;
+ void (*op)(int ) = (void (*)(int ))(& f);
+ /*@ assert op ≡ &f; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/spec/unused_parameter_attribute.i b/tests/spec/unused_parameter_attribute.i
new file mode 100644
index 00000000000..b5d0d5b87f1
--- /dev/null
+++ b/tests/spec/unused_parameter_attribute.i
@@ -0,0 +1,6 @@
+void f(int a __attribute__((unused)) );
+
+int main(void){
+ void (*op) (int) = f ;
+ //@ assert op == f ;
+}
--
GitLab