[parser] Better message for attribute annotation errors

src/kernel_internals/parsing/logic_parser.mly

@@ -1372,6 +1372,11 @@ annot:
 | decl_list EOF   { Adecl ($1) }
 ;
 
+// Not supported anymore
+attribute_annot:
+| identifier { $1 }
+| GHOST { "\\ghost" }
+
 annotation:
 | loop_annotations
       { let (b,v,p) = $1 in
@@ -1386,6 +1391,11 @@ annotation:
           (Not_well_formed (loc $sloc,
                             "Only one code annotation is allowed per comment"))
       }
+| attribute_annot {
+    raise (Not_well_formed (loc $sloc,
+      "Attribute annotation '"^ $1 ^"' are not supported anymore, use regular \
+       C attributes instead."))
+  }
 | unknown_extension SEMICOLON { raise Unknown_ext }
 ;
 
@@ -2078,7 +2088,6 @@ bs_keyword:
 | AS { () }
 | BASE_ADDR { () }
 | BLOCK_LENGTH { () }
-| GHOST { () }
 | DYNAMIC { () }
 | EMPTY { () }
 | FALSE { () }
@@ -2086,6 +2095,7 @@ bs_keyword:
 | FREEABLE { () }
 | FRESH { () }
 | FROM { () }
+| GHOST { () }
 | INTER { () }
 | LAMBDA { () }
 | LET { () }

tests/spec/oracle/ghost_attribute.res.oracle

 [kernel] Parsing ghost_attribute.i (no preprocessing)
 [kernel:annot-error] ghost_attribute.i:15: Warning: 
-  unexpected token 'my_attribute'
+  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
 [kernel:annot-error] ghost_attribute.i:16: Warning: 
-  unexpected token 'my_attribute'
+  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
 [kernel:annot-error] ghost_attribute.i:20: Warning: 
-  unexpected token 'my_attribute'
+  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
 [kernel:annot-error] ghost_attribute.i:21: Warning: 
-  unexpected token 'my_attribute'
+  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
 [kernel:unknown-attribute] ghost_attribute.i:28: Warning: 
   Unknown attribute: unregistered_attr
 [kernel:unknown-attribute] ghost_attribute.i:29: Warning: 

tests/spec/oracle/parsing.res.oracle

 [kernel] Parsing parsing.c (with preprocessing)
-[kernel:annot-error] parsing.c:27: Warning: unexpected token 'private'
+[kernel:annot-error] parsing.c:27: Warning: 
+  Attribute annotation 'private' are not supported anymore, use regular C attributes instead.
 [kernel:annot-error] parsing.c:15: Warning: 
   comparison of incompatible types: 𝔹 and ℤ. Ignoring global annotation
 [kernel:annot-error] parsing.c:19: Warning: 

tests/syntax/ghost_cv_parsing_errors.c

@@ -23,6 +23,8 @@ int \ghost global ;
 
 #ifdef IN_GHOST_ATTR
 
+// Attribute annotation are not supported anymore, any keyword or identifier
+// Here will produce the same error.
 int /*@ \ghost */ global ;
 
 #endif

tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle

 [kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
-[kernel:annot-error] ghost_cv_parsing_errors.c:26: Warning: 
-  unexpected token '\ghost'
+[kernel:annot-error] ghost_cv_parsing_errors.c:28: Warning: 
+  Attribute annotation '\ghost' are not supported anymore, use regular C attributes instead.
 [kernel] User Error: warning annot-error treated as fatal error.
 [kernel] Frama-C aborted: invalid user input.