default_spec_mode.0.res.oracle

[kernel] Parsing default_spec_mode.i (no preprocessing)
/* Generated by Frama-C */
void f1(void);

void f2(void)
{
  f1();
  return;
}

/*@ requires \true; */
int f3(int *a);

/*@ requires \true;
    assigns *b; */
int f4(int *b)
{
  int tmp;
  tmp = f3(b);
  return tmp;
}