/* 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 scanf_format {
   int *p_int ;
   double *p_double ;
   long *p_long ;
   unsigned int *p_uint ;
   unsigned long *p_ulong ;
   char *p_char ;
   short *p_short ;
   long long *p_longlong ;
   unsigned long long *p_ulonglong ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
extern int ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments )  printf)(char const   * __restrict  __format 
                                                                                 , ...) ;
struct meta_wildp_int {
   void *_b ;
}   ;
struct wildp_int {
   int * __WILD  _p ;
   struct meta_wildp_int _ms ;
}   ;
typedef struct wildp_int wildp_int;
struct _tagged_a_wildp_int {
   unsigned int _len ;
   wildp_int ( __WILD  _data)[8]  __attribute__((__packed__)) ;
   int _tags[(sizeof(wildp_int /* __WILD  */[8]) + 127U) >> 7]  __attribute__((__packed__)) ;
};
typedef struct _tagged_a_wildp_int _tagged_a_wildp_int;
_tagged_a_wildp_int a_t  __TAGGED   =    {(sizeof(wildp_int /* __WILD  */[8]) + 3U) >> 2};
extern int __ccured_va_count ;
static char __string1[18]  = 
  {      'a',      ' ',      'h',      'a', 
        's',      ' ',      '%',      'd', 
        ' ',      'e',      'l',      'e', 
        'm',      'e',      'n',      't', 
        's',      '\000'};
void so_and_so_code(int **x ) ;
void so_and_so_code(int **x ) 
{ int * __WILD  pa ;
  int * __WILD  __cil_tmp3 ;
  void *pa_b6 ;
  void *__cil_tmp3_b7 ;

  {
  pa_b6 = (void *)0;
  __cil_tmp3 = (int */* __WILD  */)(& a_t._data[0]);
  __cil_tmp3_b7 = & a_t._data;
  pa_b6 = __cil_tmp3_b7;
  pa = __cil_tmp3;
  __ccured_va_count = -1;
  printf((char const   */* __restrict  */)((char const   */* __restrict  */)(& __string1[0])),
         (int )(sizeof(a_t._data) / sizeof(int *)));
  return;
}
}