Skip to content
Snippets Groups Projects
Commit 23b45ada authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/kernel/attr-annot' into 'master'

Fixes attribute annotations for formals

See merge request frama-c/frama-c!3072
parents c607ca91 adcb06b9
No related branches found
No related tags found
No related merge requests found
......@@ -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,
......
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