diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 26a088776423753ffba37c1c13e53a6c59c29455..11d9ae4dbcd3c6a7af92e7f44b7412d1a2585836 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 0000000000000000000000000000000000000000..c37c677382b047333351dea224fa8291d6856daa
--- /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 0000000000000000000000000000000000000000..4a38d813d2571f4dec979f144c0684caf35120fc
--- /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;
+}
+
+