Skip to content
Snippets Groups Projects
Commit adcb06b9 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[kernel] Fixes attribute annotations for formals

parent c607ca91
No related branches found
No related tags found
No related merge requests found
...@@ -1528,7 +1528,7 @@ attribute: ...@@ -1528,7 +1528,7 @@ attribute:
| VOLATILE { ("volatile",[]), $1 } | VOLATILE { ("volatile",[]), $1 }
| GHOST { ("ghost",[]), $1 } | GHOST { ("ghost",[]), $1 }
| ATTRIBUTE_ANNOT { let annot, loc = $1 in | 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, /* (* sm: I need something that just includes __attribute__ and nothing more,
......
void foo(int* p /*@ my_attribute */){
int /*@ my_attribute */ v ;
}
[kernel] Parsing tests/spec/ghost_attribute.i (no preprocessing)
/* Generated by Frama-C */
void foo(int *p /*@ my_attribute */)
{
int /*@ my_attribute */ v;
return;
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment