/* 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 ;
};
struct _sized_a_p_int {
   unsigned int _size ;
   int *( __SIZED  _array)[0]  __attribute__((__packed__)) ;
};
typedef struct _sized_a_p_int _sized_a_p_int;
struct open {
   int count ;
   _sized_a_p_int __SIZED   rest ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
struct meta_fseqp_void {
   void *_e ;
}   ;
struct fseqp_void {
   void * __FSEQ  _p ;
   struct meta_fseqp_void _ms ;
}   ;
typedef struct fseqp_void fseqp_void;
extern fseqp_void malloc_f(unsigned int  ) ;
struct meta_fseqp_s_open {
   void *_e ;
}   ;
struct fseqp_s_open {
   struct open * __FSEQ  _p ;
   struct meta_fseqp_s_open _ms ;
}   ;
typedef struct fseqp_s_open fseqp_s_open;
int main(void) ;
int main(void) 
{ fseqp_s_open p ;
  struct fseqp_s_open tmp ;
  int __retres3 ;
  fseqp_void __cil_tmp4 ;
  struct fseqp_s_open __cil_tmp5 ;
  fseqp_s_open __cil_tmp6 ;
  fseqp_s_open __cil_tmp7 ;
  void *__cil_tmp8 ;

  {
  tmp._ms._e = (void *)0;
  tmp._p = (struct open */* __FSEQ  */)0;
  p._ms._e = (void *)0;
  p._p = (struct open */* __FSEQ  */)0;
  __ccuredAlwaysStopOnError = 0;
  __ccuredUseStrings = 1;
  __ccuredLogNonPointers = 0;
  __ccuredInit();
  __cil_tmp4 = malloc_f(20U);
  CHECK_FSEQALIGN(sizeof(struct open ), (void *)((struct open */* __FSEQ  */)__cil_tmp4._p),
                  __cil_tmp4._ms._e);
  __cil_tmp5._p = (struct open */* __FSEQ  */)__cil_tmp4._p;
  __cil_tmp5._ms._e = __cil_tmp4._ms._e;
  tmp = __cil_tmp5;
  __cil_tmp6._p = tmp._p;
  __cil_tmp6._ms._e = tmp._ms._e;
  p = __cil_tmp6;
  CHECK_FSEQARITH((void *)p._p, sizeof(struct open ), (void *)(p._p + 1), p._ms._e,
                  0);
  __cil_tmp7._p = p._p + 1;
  __cil_tmp7._ms._e = p._ms._e;
  p = __cil_tmp7;
  CHECK_FSEQ2SAFE(p._ms._e, (void *)p._p, sizeof(struct open ), sizeof(struct open ),
                  1, 0);
  __cil_tmp8 = CHECK_FETCH_INDEX_END((void *)(& (p._p)->rest._array[5]), (void *)((p._p)->rest._array),
                                     0);
  CHECK_SEQ2SAFE((void *)((p._p)->rest._array), __cil_tmp8, (void *)(& (p._p)->rest._array[5]),
                 sizeof(int *), sizeof(int *), 1, 1);
  __retres3 = (int )(p._p)->rest._array[5];
  return (__retres3);
}
}