static char const   *c  =    (char const   *)"Booting";
  
extern int strlen(char * ) ;

int main(void) {
  char *_cil_inline_tmp_218 ;
  int _cil_inline_tmp_219 ;
   
   _cil_inline_tmp_218 = (char *)c;
   _cil_inline_tmp_219 = strlen(_cil_inline_tmp_218);

   return 0;
}