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

#define CCURED_SPLIT_ARGUMENTS
// #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 _tagged_a_int {
   unsigned int _len ;
   int ( __WILD  _data)[8]  __attribute__((__packed__)) ;
   int _tags[(sizeof(int /* __WILD  */[8]) + 127U) >> 7]  __attribute__((__packed__)) ;
};
typedef struct _tagged_a_int _tagged_a_int;
_tagged_a_int data_t  __TAGGED   =    {(sizeof(int /* __WILD  */[8]) + 3U) >> 2};
struct meta_wildp_void {
   void *_b ;
}   ;
struct wildp_void {
   void * __WILD  _p ;
   struct meta_wildp_void _ms ;
}   ;
typedef struct wildp_void wildp_void;
wildp_void myalloc_w(int sz ) ;
wildp_void myalloc_w(int sz ) 
{ void * __WILD  __retres2 ;
  void * __WILD  __cil_tmp3 ;
  wildp_void __cil_tmp4 ;
  void *__retres2_b7 ;
  void *__cil_tmp3_b8 ;

  {
  __retres2_b7 = (void *)0;
  __cil_tmp3 = (void */* __WILD  */)(& data_t._data[0]);
  __cil_tmp3_b8 = & data_t._data;
  __retres2_b7 = __cil_tmp3_b8;
  __retres2 = __cil_tmp3;
  __cil_tmp4._p = __retres2;
  __cil_tmp4._ms._b = __retres2_b7;
  return (__cil_tmp4);
}
}
struct meta_wildp_int___0 {
   void *_b ;
}   ;
struct wildp_int___0 {
   int * __WILD  _p ;
   struct meta_wildp_int___0 _ms ;
}   ;
typedef struct wildp_int___0 wildp_int___0;
struct meta_wildp_p_int {
   void *_b ;
}   ;
int main(void) ;
int main(void) 
{ wildp_int___0 * __WILD  p ;
  wildp_int___0 * __WILD  tmp ;
  int __retres3 ;
  wildp_void __cil_tmp4 ;
  wildp_int___0 * __WILD  __cil_tmp5 ;
  wildp_int___0 * __WILD  __cil_tmp6 ;
  unsigned int _tlen7 ;
  unsigned int _tlen8 ;
  unsigned int _tlen9 ;
  void *p_b14 ;
  void *tmp_b15 ;
  void *__cil_tmp5_b16 ;
  void *__cil_tmp6_b17 ;

  {
  tmp_b15 = (void *)0;
  p_b14 = (void *)0;
  __ccuredAlwaysStopOnError = 0;
  __ccuredUseStrings = 1;
  __ccuredLogNonPointers = 0;
  __ccuredInit();
  __cil_tmp4 = myalloc_w(8);
  __cil_tmp5 = (wildp_int___0 */* __WILD  */)__cil_tmp4._p;
  __cil_tmp5_b16 = __cil_tmp4._ms._b;
  tmp_b15 = __cil_tmp5_b16;
  tmp = __cil_tmp5;
  __cil_tmp6 = tmp;
  __cil_tmp6_b17 = tmp_b15;
  p_b14 = __cil_tmp6_b17;
  p = __cil_tmp6;
  _tlen7 = CHECK_FETCHLENGTH((void *)(& data_t._data[1]), (void *)(& data_t._data),
                             0);
  CHECK_BOUNDS_LEN((void *)(& data_t._data), _tlen7, (void *)(& data_t._data[1]),
                   sizeof(int ), sizeof(int ));
  CHECK_ZEROTAGS((void *)(& data_t._data), _tlen7, (void *)(& data_t._data[1]), sizeof(int ));
  data_t._data[1] = 5;
  _tlen8 = CHECK_FETCHLENGTH((void *)(p + 1), p_b14, 0);
  CHECK_BOUNDS_LEN(p_b14, _tlen8, (void *)(p + 1), sizeof(wildp_int___0 ), sizeof(wildp_int___0 ));
  CHECK_WILDPOINTERREAD(p_b14, _tlen8, (void *)(p + 1));
  _tlen9 = CHECK_FETCHLENGTH((void *)(p + 1)->_p, (p + 1)->_ms._b, 0);
  CHECK_BOUNDS_LEN((p + 1)->_ms._b, _tlen9, (void *)(p + 1)->_p, sizeof(int ), sizeof(int ));
  __retres3 = *((p + 1)->_p);
  return (__retres3);
}
}