ghost_attribute.res.oracle

[kernel] Parsing ghost_attribute.i (no preprocessing)
[kernel:annot-error] ghost_attribute.i:15: Warning: 
  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
[kernel:annot-error] ghost_attribute.i:16: Warning: 
  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
[kernel:annot-error] ghost_attribute.i:20: Warning: 
  Attribute annotation 'my_attribute' are not supported anymore, use regular C attributes instead.
[kernel:annot-error] ghost_attribute.i:21: Warning: 
  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: 
  Unknown attribute: unregistered_attr
[kernel:unknown-attribute] ghost_attribute.i:33: Warning: 
  Unknown attribute: unregistered_attr
[kernel:unknown-attribute] ghost_attribute.i:34: Warning: 
  Unknown attribute: unregistered_attr
/* Generated by Frama-C */
void attr_annot(int *p)
{
  int v;
  return;
}

/*@ ghost void attr_annot_ghost(int *p)
          {
            int v;
            return;
          }

*/

void unregistered_attr(int *p __attribute__((__unregistered_attr__)))
{
  int __attribute__((__unregistered_attr__)) v;
  return;
}

/*@ ghost
  void unregistered_attr_ghost(int *p __attribute__((__unregistered_attr__)))
  {
    int __attribute__((__unregistered_attr__)) v;
    return;
  }

*/

void registered_attr(int * __attribute__((__registered_attr__)) p)
{
  int __attribute__((__registered_attr__)) v;
  return;
}

/*@ ghost
  void registered_attr_ghost(int * __attribute__((__registered_attr__)) p)
  {
    int __attribute__((__registered_attr__)) v;
    return;
  }

*/