diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 23900b640933ece2d12960901d2e8f5bce7b1697..3667813a8fb107fef01c5fbb8622c597d12e7989 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 0000000000000000000000000000000000000000..809fe3405fb8cc684a82625d3647c12c24f7210e
--- /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 0000000000000000000000000000000000000000..b5d0d5b87f1024f7c594b5fc13fb664c706348df
--- /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 ;
+}