const-assignments.0.res.oracle

[kernel] Parsing const-assignments.c (with preprocessing)
/* Generated by Frama-C */
struct S {
   int x ;
   int const y ;
   struct S *z[3] ;
};
typedef struct S S;
int const x = 1;
extern void g(int *p);

void h(int const *x_0)
{
  int *y = (int *)x_0;
  *y = 1;
  g(y);
  return;
}

void build_S(S const *s, int x_0, int y)
{
  s->x = x_0;
  s->y = y;
  return;
}

void mutable_test(S const *s)
{
  s->x = 42;
  (s->x) ++;
  s->x += 2;
  return;
}

extern void k1(S *);

extern void k2(int *);

void mutable_test_call(S const *s)
{
  k1((S *)s);
  k1(s->z[0]);
  int a = 1;
  k1((S *)((s + 2) + a));
  k2((int *)(& (s + 2)->y));
  return;
}