assign5.res.oracle

[kernel] Parsing tests/rte/assign5.c (with preprocessing)
[rte] annotating function main
/* Generated by Frama-C */
/*@ assigns *p, *p;
    assigns *p \from x;
    assigns *p \from \nothing; */
int f(int *p, int x);

/*@ assigns *p, *p;
    assigns *p \from \nothing;
    assigns *p \from x; */
int g(int *p, int x);

int main(void)
{
  int __retres;
  int i;
  int a;
  int t[10];
  i = 0;
  a = 0;
  t[0] = f(& i,a);
  t[1] = g(& i,a);
  __retres = 0;
  return __retres;
}