void debug_exit(int result);
debug_exit causes the debugger to exit and result is returned to the user.