/* Generated by CIL v. 1.3.5 */
/* print_CIL_Input is false */

// #define CCURED_ALLOW_PARTIAL_ELEMENTS_IN_SEQUENCE
// #define CCURED_LOG_NON_POINTERS
#define CCURED_USE_STRINGS
// #define CCURED_FAIL_IS_TERSE
// #define CCURED_ALWAYS_STOP_ON_ERROR
// Include the definition of the checkers
#define CCURED
#define CCURED_POST
#include "ccuredcheck.h"
struct printf_arguments {
   int i ;
   double d ;
   char * __ROSTRING  s ;
   long long ll ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
struct meta_seq_void {
   void *_b ;
   void *_e ;
}   ;
struct seq_void {
   void * __SEQ  _p ;
   struct meta_seq_void _ms ;
}   ;
typedef struct seq_void seq_void;
extern seq_void malloc_q(unsigned int  ) ;
struct meta_seq_int {
   void *_b ;
   void *_e ;
}   ;
struct seq_int {
   int * __SEQ  _p ;
   struct meta_seq_int _ms ;
}   ;
typedef struct seq_int seq_int;
struct meta_seq_int___0 {
   void *_b ;
   void *_e ;
}   ;
struct seq_int___0 {
   int * __SEQ  _p ;
   struct meta_seq_int___0 _ms ;
}   ;
typedef struct seq_int___0 seq_int___0;
int foo(int x ) ;
int foo(int x ) 
{ seq_int p ;
  seq_int___0 r1 ;
  struct seq_int r2 ;
  int ( __SEQ  a)[8] ;
  int __retres7 ;
  seq_void __cil_tmp9 ;
  seq_int___0 __cil_tmp10 ;
  struct seq_int __cil_tmp11 ;
  seq_int __cil_tmp12 ;
  seq_int __cil_tmp13 ;

  {
  r2._ms._e = (void *)0;
  r2._ms._b = (void *)0;
  r2._p = (int */* __SEQ  */)0;
  r1._ms._e = (void *)0;
  r1._ms._b = (void *)0;
  r1._p = (int */* __SEQ  */)0;
  p._ms._e = (void *)0;
  p._ms._b = (void *)0;
  p._p = (int */* __SEQ  */)0;
  __cil_tmp9 = malloc_q(16U);
  CHECK_SEQALIGN(sizeof(int ), (void *)((int */* __SEQ  */)__cil_tmp9._p), __cil_tmp9._ms._b,
                 __cil_tmp9._ms._e);
  __cil_tmp10._p = (int */* __SEQ  */)__cil_tmp9._p;
  __cil_tmp10._ms._b = __cil_tmp9._ms._b;
  __cil_tmp10._ms._e = __cil_tmp9._ms._e;
  r1 = __cil_tmp10;
  __cil_tmp11._p = (int */* __SEQ  */)(a);
  __cil_tmp11._ms._b = a;
  __cil_tmp11._ms._e = a + 8;
  r2 = __cil_tmp11;
  __cil_tmp12._p = (int */* __SEQ  */)r1._p;
  __cil_tmp12._ms._b = r1._ms._b;
  __cil_tmp12._ms._e = r1._ms._e;
  p = __cil_tmp12;
  __cil_tmp13._p = r2._p;
  __cil_tmp13._ms._b = r2._ms._b;
  __cil_tmp13._ms._e = r2._ms._e;
  p = __cil_tmp13;
  CHECK_SEQ2SAFE(p._ms._b, p._ms._e, (void *)(p._p + x), sizeof(int ), sizeof(int ),
                 1, 0);
  __retres7 = *(p._p + x);
  return (__retres7);
}
}