void *
get_ret_code (void)
{
  return (void *) (int) 42;
}