array_formals.res.oracle

[kernel] Parsing array_formals.i (no preprocessing)
[kernel:unknown-attribute] array_formals.i:7: Warning: Unknown attribute: test
/* Generated by Frama-C */
typedef int ( __attribute__((__test__)) arr)[2];
int f(int a[2])
{
  int __retres;
  __retres = *(a + 1);
  return __retres;
}

int g(int a[static 2])
{
  int __retres;
  __retres = *(a + 1);
  return __retres;
}

int h(int a[static const restrict 2])
{
  int __retres;
  __retres = *(a + 1);
  return __retres;
}

int k(int ( __attribute__((__test__)) a)[2])
{
  int __retres;
  __retres = *(a + 1);
  return __retres;
}

int l(void)
{
  int tmp;
  arr a = {0};
  tmp = k(a);
  return tmp;
}