decl-function.res.oracle

[kernel] Parsing decl-function.i (no preprocessing)
/* Generated by Frama-C */
int x;
void (*pf)(void);
extern void f_undefined(void);

void g(void)
{
  f_undefined();
  /*@ assert fcs_limitation: pf == &f_undefined; */ ;
  return;
}

/*@ logic integer foo(integer y) = y;

*/
/*@ requires fcs_limitation: pf == &f_undefined;
    ensures x == foo(x); */
extern void f_undefined(void);

void main(void)
{
  pf = & f_undefined;
  f_undefined();
  f_undefined();
  return;
}