access_volatile_bts1589.res.oracle

[kernel] Parsing access_volatile_bts1589.i (no preprocessing)
/* Generated by Frama-C */
typedef int volatile vi;
struct volatile_struct {
   int volatile a ;
   vi b ;
   int c ;
};
int volatile x;
int z;
vi y;
struct volatile_struct vs;
int main(void)
{
  int __retres;
  int tmp = x;
  int tmp_3 = y;
  int tmp_5 = vs.a;
  int tmp_7 = vs.b;
  __retres = 0;
  return __retres;
}