/* 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 ;
};
struct bar {
   int nrInts ;
   int * __COUNT(nrInts)  ints ;
};
struct foo {
   int sizeBars ;
   struct bar * __SIZE(sizeBars)  bars ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
extern unsigned int /*2*/malloc(int  ) ;
struct meta_fseqp_void {
   void *_e ;
}   ;
extern void */*3*/__ptrof_size_sf(void * __FSEQ  ptr_p , void *ptr_ms_e , unsigned int size ) ;
struct meta_fseqp_s_bar {
   void *_e ;
}   ;
void init(struct foo *pFoo ) ;
void init(struct foo *pFoo ) 
{ int nrBars ;
  struct bar * __SIZE(sizeBars)  bars_withsize4 ;
  struct bar * __FSEQ __SIZE(sizeBars)  bars_withsize5 ;
  void *__cil_tmp6 ;
  struct bar * __FSEQ __SIZE(sizeBars)  __cil_tmp7 ;
  struct bar * __FSEQ __SIZE(sizeBars)  __cil_tmp8 ;
  unsigned int __cil_tmp9 ;
  struct bar * __FSEQ __SIZE(sizeBars)  __cil_tmp10 ;
  void * __FSEQ  __cil_tmp11 ;
  void *__cil_tmp12 ;
  void *bars_withsize5_e17 ;
  void *__cil_tmp7_e18 ;
  void *__cil_tmp10_e19 ;
  void *__cil_tmp11_e20 ;

  {
  bars_withsize5_e17 = (void *)0;
  bars_withsize5 = (struct bar */* __FSEQ __SIZE(sizeBars)  */)0;
  bars_withsize4 = (struct bar */* __SIZE(sizeBars)  */)0;
  nrBars = 5;
  CHECK_NULL((void *)pFoo);
  __cil_tmp6 = (void *)pFoo->bars;
  bars_withsize4 = (struct bar */* __SIZE(sizeBars)  */)__cil_tmp6;
  pFoo->bars = (struct bar */* __SIZE(sizeBars)  */)0;
  pFoo->sizeBars = (int )((unsigned int )nrBars * sizeof(*bars_withsize4));
  __cil_tmp8 = (struct bar */* __FSEQ __SIZE(sizeBars)  */)/*2*/malloc((((unsigned int )pFoo->sizeBars + 3U) >> 2) << 2);
  if (__cil_tmp8) {

    __cil_tmp7 = __cil_tmp8;


    __cil_tmp9 = (unsigned int )__cil_tmp8 + ((((unsigned int )pFoo->sizeBars + 3U) >> 2) << 2);

    while ((unsigned int )__cil_tmp8 + sizeof(struct bar ) <= __cil_tmp9) {
      __cil_tmp8->ints = (int */* __COUNT(nrInts)  */)0;
      __cil_tmp8 ++;
    }
    __cil_tmp7_e18 = __cil_tmp8;
  } else {
    __cil_tmp7 = 0;
    __cil_tmp7_e18 = (void *)0;
  }
  __cil_tmp10 = __cil_tmp7;
  __cil_tmp10_e19 = __cil_tmp7_e18;
  bars_withsize5_e17 = __cil_tmp10_e19;
  bars_withsize5 = __cil_tmp10;
  __cil_tmp11 = (void */* __FSEQ  */)bars_withsize5;
  __cil_tmp11_e20 = bars_withsize5_e17;
  CHECK_NULL((void *)pFoo);
  __cil_tmp12 = /*3*/__ptrof_size_sf(__cil_tmp11, __cil_tmp11_e20, (unsigned int )pFoo->sizeBars);
  pFoo->bars = (struct bar */* __SIZE(sizeBars)  */)__cil_tmp12;
  return;
}
}