assign5.res.oracle

[kernel] Parsing assign5.c (with preprocessing)
[kernel:annot:multi-from] Warning: 
  Drop '*p' \from at assign5.c:9 for more precise one at assign5.c:10
[kernel:annot:multi-from] Warning: 
  Drop '*p' \from at assign5.c:19 for more precise one at assign5.c:18
[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ assigns *p;
    assigns *p \from \nothing; */
int f(int *p, int x);

/*@ assigns *p;
    assigns *p \from \nothing; */
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;
}