/* 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 meta_wildp_int {
   void *_b ;
}   ;
struct wildp_int {
   int * __WILD  _p ;
   struct meta_wildp_int _ms ;
}   ;
typedef struct wildp_int wildp_int;
struct __anonstruct_f3_2 {
   wildp_int a1 ;
   int a2 ;
   struct wildp_int a3 ;
};
union __anonunion_x_1 {
   struct wildp_int f1 ;
   struct wildp_int ( __WILD  f2)[2] ;
   struct __anonstruct_f3_2 f3 ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
union __anonunion_x_1 *x  ;
struct wildp_int foo_w(void) ;
struct wildp_int foo_w(void) 
{ int * __WILD  __retres1 ;
  int * __WILD  __cil_tmp2 ;
  struct wildp_int __cil_tmp3 ;
  void *__retres1_b6 ;
  void *__cil_tmp2_b7 ;

  {
  __retres1_b6 = (void *)0;
  CHECK_NULL((void *)x);
  __cil_tmp2 = x->f1._p;
  __cil_tmp2_b7 = x->f1._ms._b;
  __retres1_b6 = __cil_tmp2_b7;
  __retres1 = __cil_tmp2;
  __cil_tmp3._p = __retres1;
  __cil_tmp3._ms._b = __retres1_b6;
  return (__cil_tmp3);
}
}