/* 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 elem {
   int f1 ;
   int f2 ;
   int ( __SEQ  nested)[8] ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
struct meta_seq_s_elem {
   void *_b ;
   void *_e ;
}   ;
struct seq_s_elem {
   struct elem * __SEQ  _p ;
   struct meta_seq_s_elem _ms ;
}   ;
typedef struct seq_s_elem seq_s_elem;
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;
int foo_q(seq_s_elem array , int len ) ;
int foo_q(seq_s_elem array , int len ) 
{ int *pnested ;
  seq_int pnestedseq ;
  int __retres5 ;
  seq_s_elem __cil_tmp6 ;
  seq_int __cil_tmp7 ;
  seq_int __cil_tmp8 ;

  {
  pnestedseq._ms._e = (void *)0;
  pnestedseq._ms._b = (void *)0;
  pnestedseq._p = (int */* __SEQ  */)0;
  pnested = (int *)0;
  CHECK_SEQARITH(sizeof(struct elem ), (void *)(array._p + len), array._ms._b, array._ms._e);
  __cil_tmp6._p = array._p + len;
  __cil_tmp6._ms._b = array._ms._b;
  __cil_tmp6._ms._e = array._ms._e;
  array = __cil_tmp6;
  CHECK_SEQ2SAFE(array._ms._b, array._ms._e, (void *)array._p, sizeof(struct elem ),
                 sizeof(struct elem ), 0, 0);
  pnested = (int *)(& (array._p)->f2);
  __cil_tmp7._p = (int */* __SEQ  */)(& (array._p)->nested[2]);
  __cil_tmp7._ms._b = (array._p)->nested;
  __cil_tmp7._ms._e = (array._p)->nested + 8;
  pnestedseq = __cil_tmp7;
  __cil_tmp8._p = pnestedseq._p + len;
  __cil_tmp8._ms._b = pnestedseq._ms._b;
  __cil_tmp8._ms._e = pnestedseq._ms._e;
  pnestedseq = __cil_tmp8;
  __retres5 = 0;
  return (__retres5);
}
}