From adcb06b933dc856aa3e278e6865e1fdac51d0242 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 15 Feb 2021 15:02:18 +0100
Subject: [PATCH] [kernel] Fixes attribute annotations for formals
---
src/kernel_internals/parsing/cparser.mly | 2 +-
tests/spec/ghost_attribute.i | 3 +++
tests/spec/oracle/ghost_attribute.res.oracle | 9 +++++++++
3 files changed, 13 insertions(+), 1 deletion(-)
create mode 100644 tests/spec/ghost_attribute.i
create mode 100644 tests/spec/oracle/ghost_attribute.res.oracle
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 26a08877642..11d9ae4dbcd 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -1528,7 +1528,7 @@ attribute:
| VOLATILE { ("volatile",[]), $1 }
| GHOST { ("ghost",[]), $1 }
| ATTRIBUTE_ANNOT { let annot, loc = $1 in
- ("$annot:" ^ annot, []), loc }
+ (Cil.mkAttrAnnot annot, []), loc }
;
/* (* sm: I need something that just includes __attribute__ and nothing more,
diff --git a/tests/spec/ghost_attribute.i b/tests/spec/ghost_attribute.i
new file mode 100644
index 00000000000..c37c677382b
--- /dev/null
+++ b/tests/spec/ghost_attribute.i
@@ -0,0 +1,3 @@
+void foo(int* p /*@ my_attribute */){
+ int /*@ my_attribute */ v ;
+}
diff --git a/tests/spec/oracle/ghost_attribute.res.oracle b/tests/spec/oracle/ghost_attribute.res.oracle
new file mode 100644
index 00000000000..4a38d813d25
--- /dev/null
+++ b/tests/spec/oracle/ghost_attribute.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing tests/spec/ghost_attribute.i (no preprocessing)
+/* Generated by Frama-C */
+void foo(int *p /*@ my_attribute */)
+{
+ int /*@ my_attribute */ v;
+ return;
+}
+
+
--
GitLab