自学教程：C++ IF函数代码示例

                                        void *P1_0(void *__cs_param_P1_arg)                                        {IF(2,0,tP1_0_1)                                        __CSEQ_atomic_begin();tP1_0_1: IF(2,1,tP1_0_2)                                        x$w_buff1 = x$w_buff0;tP1_0_2: IF(2,2,tP1_0_3)                                        x$w_buff0 = 2;tP1_0_3: IF(2,3,tP1_0_4)                                        x$w_buff1_used = x$w_buff0_used;tP1_0_4: IF(2,4,tP1_0_5)                                        x$w_buff0_used = (_Bool) 1;tP1_0_5: IF(2,5,tP1_0_6)                                        assert(!(x$w_buff1_used && x$w_buff0_used));tP1_0_6: IF(2,6,tP1_0_7)                                        x$r_buff1_thd0 = x$r_buff0_thd0;tP1_0_7: IF(2,7,tP1_0_8)                                        x$r_buff1_thd1 = x$r_buff0_thd1;tP1_0_8: IF(2,8,tP1_0_9)                                        x$r_buff1_thd2 = x$r_buff0_thd2;tP1_0_9: IF(2,9,tP1_0_10)                                        x$r_buff0_thd2 = (_Bool) 1;                                        __CSEQ_atomic_end();tP1_0_10: IF(2,10,tP1_0_11)                                        __CSEQ_atomic_begin();tP1_0_11: IF(2,11,tP1_0_12)                                        y = 1;                                        __CSEQ_atomic_end();tP1_0_12: IF(2,12,tP1_0_13)                                        __CSEQ_atomic_begin();tP1_0_13: IF(2,13,tP1_0_14)                                        __unbuffered_p1_EAX = y;                                        __CSEQ_atomic_end();tP1_0_14: IF(2,14,tP1_0_15)                                        __CSEQ_atomic_begin();tP1_0_15: IF(2,15,tP1_0_16)                                        __unbuffered_p1_EBX = z;                                        __CSEQ_atomic_end();tP1_0_16: IF(2,16,tP1_0_17)                                        __CSEQ_atomic_begin();tP1_0_17: IF(2,17,tP1_0_18)                                        x = x$w_buff0_used && x$r_buff0_thd2 ? x$w_buff0 : x$w_buff1_used && x$r_buff1_thd2 ? x$w_buff1 : x;tP1_0_18: IF(2,18,tP1_0_19)                                        x$w_buff0_used = x$w_buff0_used && x$r_buff0_thd2 ? (_Bool) 0 : x$w_buff0_used;tP1_0_19: IF(2,19,tP1_0_20)                                        x$w_buff1_used = (x$w_buff0_used && x$r_buff0_thd2) || (x$w_buff1_used && x$r_buff1_thd2) ? (_Bool) 0 : x$w_buff1_used;tP1_0_20: IF(2,20,tP1_0_21)                                        x$r_buff0_thd2 = x$w_buff0_used && x$r_buff0_thd2 ? (_Bool) 0 : x$r_buff0_thd2;tP1_0_21: IF(2,21,tP1_0_22)                                        x$r_buff1_thd2 = (x$w_buff0_used && x$r_buff0_thd2) || (x$w_buff1_used && x$r_buff1_thd2) ? (_Bool) 0 : x$r_buff1_thd2;                                        __CSEQ_atomic_end();tP1_0_22: IF(2,22,tP1_0_23)                                        __CSEQ_atomic_begin();tP1_0_23: IF(2,23,tP1_0_24)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P1;                                        		;                                        __exit_P1:                                        		__CPROVER_assume(__cs_pc_cs[2] >= 24);                                        		;                                        		;tP1_0_24:                                         STOP_NONVOID(24);                                        }

voidvec4_gs_visitor::gs_emit_vertex(int stream_id){    this->current_annotation = "emit vertex: safety check";    /* Haswell and later hardware ignores the "Render Stream Select" bits     * from the 3DSTATE_STREAMOUT packet when the SOL stage is disabled,     * and instead sends all primitives down the pipeline for rasterization.     * If the SOL stage is enabled, "Render Stream Select" is honored and     * primitives bound to non-zero streams are discarded after stream output.     *     * Since the only purpose of primives sent to non-zero streams is to     * be recorded by transform feedback, we can simply discard all geometry     * bound to these streams when transform feedback is disabled.     */    if (stream_id > 0 && !nir->info->has_transform_feedback_varyings)        return;    /* If we're outputting 32 control data bits or less, then we can wait     * until the shader is over to output them all.  Otherwise we need to     * output them as we go.  Now is the time to do it, since we're about to     * output the vertex_count'th vertex, so it's guaranteed that the     * control data bits associated with the (vertex_count - 1)th vertex are     * correct.     */    if (c->control_data_header_size_bits > 32) {        this->current_annotation = "emit vertex: emit control data bits";        /* Only emit control data bits if we've finished accumulating a batch         * of 32 bits.  This is the case when:         *         *     (vertex_count * bits_per_vertex) % 32 == 0         *         * (in other words, when the last 5 bits of vertex_count *         * bits_per_vertex are 0).  Assuming bits_per_vertex == 2^n for some         * integer n (which is always the case, since bits_per_vertex is         * always 1 or 2), this is equivalent to requiring that the last 5-n         * bits of vertex_count are 0:         *         *     vertex_count & (2^(5-n) - 1) == 0         *         * 2^(5-n) == 2^5 / 2^n == 32 / bits_per_vertex, so this is         * equivalent to:         *         *     vertex_count & (32 / bits_per_vertex - 1) == 0         */        vec4_instruction *inst =            emit(AND(dst_null_ud(), this->vertex_count,                     brw_imm_ud(32 / c->control_data_bits_per_vertex - 1)));        inst->conditional_mod = BRW_CONDITIONAL_Z;        emit(IF(BRW_PREDICATE_NORMAL));        {            /* If vertex_count is 0, then no control data bits have been             * accumulated yet, so we skip emitting them.             */            emit(CMP(dst_null_ud(), this->vertex_count, brw_imm_ud(0u),                     BRW_CONDITIONAL_NEQ));            emit(IF(BRW_PREDICATE_NORMAL));            emit_control_data_bits();            emit(BRW_OPCODE_ENDIF);            /* Reset control_data_bits to 0 so we can start accumulating a new             * batch.             *             * Note: in the case where vertex_count == 0, this neutralizes the             * effect of any call to EndPrimitive() that the shader may have             * made before outputting its first vertex.             */            inst = emit(MOV(dst_reg(this->control_data_bits), brw_imm_ud(0u)));            inst->force_writemask_all = true;        }        emit(BRW_OPCODE_ENDIF);    }    this->current_annotation = "emit vertex: vertex data";    emit_vertex();    /* In stream mode we have to set control data bits for all vertices     * unless we have disabled control data bits completely (which we do     * do for GL_POINTS outputs that don't use streams).     */    if (c->control_data_header_size_bits > 0 &&            gs_prog_data->control_data_format ==            GEN7_GS_CONTROL_DATA_FORMAT_GSCTL_SID) {        this->current_annotation = "emit vertex: Stream control data bits";        set_stream_control_data_bits(stream_id);    }    this->current_annotation = NULL;}

                                        void *P2_0(void *__cs_param_P2_arg)                                        {IF(3,0,tP2_0_1)                                        __CSEQ_atomic_begin();tP2_0_1: IF(3,1,tP2_0_2)                                        y$w_buff1 = y$w_buff0;tP2_0_2: IF(3,2,tP2_0_3)                                        y$w_buff0 = 1;tP2_0_3: IF(3,3,tP2_0_4)                                        y$w_buff1_used = y$w_buff0_used;tP2_0_4: IF(3,4,tP2_0_5)                                        y$w_buff0_used = (_Bool) 1;tP2_0_5: IF(3,5,tP2_0_6)                                        assert(!(y$w_buff1_used && y$w_buff0_used));tP2_0_6: IF(3,6,tP2_0_7)                                        y$r_buff1_thd0 = y$r_buff0_thd0;tP2_0_7: IF(3,7,tP2_0_8)                                        y$r_buff1_thd1 = y$r_buff0_thd1;tP2_0_8: IF(3,8,tP2_0_9)                                        y$r_buff1_thd2 = y$r_buff0_thd2;tP2_0_9: IF(3,9,tP2_0_10)                                        y$r_buff1_thd3 = y$r_buff0_thd3;tP2_0_10: IF(3,10,tP2_0_11)                                        y$r_buff1_thd4 = y$r_buff0_thd4;tP2_0_11: IF(3,11,tP2_0_12)                                        y$r_buff0_thd3 = (_Bool) 1;                                        __CSEQ_atomic_end();tP2_0_12: IF(3,12,tP2_0_13)                                        __CSEQ_atomic_begin();tP2_0_13: IF(3,13,tP2_0_14)                                        __unbuffered_p2_EAX = z;                                        __CSEQ_atomic_end();tP2_0_14: IF(3,14,tP2_0_15)                                        __CSEQ_atomic_begin();tP2_0_15: IF(3,15,tP2_0_16)                                        y = y$w_buff0_used && y$r_buff0_thd3 ? y$w_buff0 : y$w_buff1_used && y$r_buff1_thd3 ? y$w_buff1 : y;tP2_0_16: IF(3,16,tP2_0_17)                                        y$w_buff0_used = y$w_buff0_used && y$r_buff0_thd3 ? (_Bool) 0 : y$w_buff0_used;tP2_0_17: IF(3,17,tP2_0_18)                                        y$w_buff1_used = (y$w_buff0_used && y$r_buff0_thd3) || (y$w_buff1_used && y$r_buff1_thd3) ? (_Bool) 0 : y$w_buff1_used;tP2_0_18: IF(3,18,tP2_0_19)                                        y$r_buff0_thd3 = y$w_buff0_used && y$r_buff0_thd3 ? (_Bool) 0 : y$r_buff0_thd3;tP2_0_19: IF(3,19,tP2_0_20)                                        y$r_buff1_thd3 = (y$w_buff0_used && y$r_buff0_thd3) || (y$w_buff1_used && y$r_buff1_thd3) ? (_Bool) 0 : y$r_buff1_thd3;                                        __CSEQ_atomic_end();tP2_0_20: IF(3,20,tP2_0_21)                                        __CSEQ_atomic_begin();tP2_0_21: IF(3,21,tP2_0_22)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P2;                                        		;                                        __exit_P2:                                        		__CPROVER_assume(__cs_pc_cs[3] >= 22);                                        		;                                        		;tP2_0_22:                                         STOP_NONVOID(22);                                        }

void* DLLEXPORT SignalGenerator_Init ( int hParentInstrumentHandle , ViRsrc szRsrcAddress , int *vhInstrumentHandle , int *InstrumentConnectStatus , int *InstrumentChannelsQuantity ){	STD_ERROR						StdError										=	{0};		tsHandle						*pLocalHandle									=	{0};		CmtTSVHandle 					handle											=	0;		int								supported										=	0;		tsSTD_CallBackSet				tSTD_CallBackSet								=	{0};		double							lfTimeout										=	0.0,									lfStateFileDelay								=	1.0,  									lfStateFileTimeout								=	10.0, 									lfDefaultTimeout								=	5.0;										IF (( szRsrcAddress == NULL ) , "Address string is empty" );		if ( hParentInstrumentHandle == 0 ) 	{		CHK_CMT ( CmtNewTSV ( sizeof(tsHandle) , &handle ));	}	else		handle = hParentInstrumentHandle;			if ( vhInstrumentHandle )		*vhInstrumentHandle = handle;		CHK_CMT ( CmtGetTSVPtr ( handle , &pLocalHandle ));	if ( pLocalHandle->defaultRM == 0 )	{		CHK_VSA ( viOpenDefaultRM (&(pLocalHandle->defaultRM)));	}		if ( pLocalHandle->sessionHandle == 0 )	{		CHK_VSA ( viOpen ( pLocalHandle->defaultRM , szRsrcAddress , VI_NULL, VI_NULL, &(pLocalHandle->sessionHandle)));	}		WaitForOperationCompletion( pLocalHandle->sessionHandle , 20.0 , 0.5 );		CHK_VSA ( viSetAttribute ( pLocalHandle->sessionHandle , VI_ATTR_TMO_VALUE , 500 ));		FREE_STDERR_COPY_ERR( Equipment_IsSupported ( pLocalHandle->sessionHandle , NULL , NULL , NULL , &supported , &pLocalHandle )); 	IF (( supported == 0 ) , "This device has not supported." );	FREE_STDERR_COPY_ERR( Equipment_Info ( pLocalHandle->sessionHandle , NULL , &pLocalHandle->pVendor , &pLocalHandle->pSerialNumber , &pLocalHandle->pModel , &pLocalHandle->pFirmware ));	STDF_UPDATE_CALLBACK_DATA(pLocalHandle->ptCallbacks); 		viPrintf( pLocalHandle->sessionHandle ,"*CLS/n" ); 		STDF_CONFIG_VALUE("Timeout", VAL_DOUBLE , 1 , lfTimeout , lfDefaultTimeout );			if ( lfTimeout == 0.0 )		lfTimeout = lfDefaultTimeout;		viSetAttribute ( pLocalHandle->sessionHandle , VI_ATTR_TMO_VALUE , (lfTimeout*1E3) );		STDF_CONFIG_VALUE("OPC_Timeout", VAL_DOUBLE , 1 , (pLocalHandle->lfTimeout) , lfDefaultTimeout );			if ( pLocalHandle->lfTimeout == 0.0 )		pLocalHandle->lfTimeout = lfDefaultTimeout;		STDF_CONFIG_VALUE("OPC_LowLevel_Timeout", VAL_DOUBLE , 1 , (pLocalHandle->lfOpcLowLevelTimeout) , lfDefaultTimeout );	 		if ( pLocalHandle->lfOpcLowLevelTimeout == 0.0 )		pLocalHandle->lfOpcLowLevelTimeout = lfDefaultTimeout;			STDF_CONFIG_VALUE("State_File_Timeout", VAL_DOUBLE , 1 , (pLocalHandle->lfStateFileTimeout) , lfStateFileTimeout );	 		if ( pLocalHandle->lfStateFileTimeout == 0.0 )		pLocalHandle->lfStateFileTimeout = lfStateFileTimeout;		STDF_CONFIG_VALUE("State_File_Delay", VAL_DOUBLE , 1 , (pLocalHandle->lfStateFileDelay) , lfStateFileDelay );	 		if ( pLocalHandle->lfStateFileDelay == 0.0 )		pLocalHandle->lfStateFileDelay = lfStateFileDelay;   Error:		if ( InstrumentConnectStatus )		*InstrumentConnectStatus = supported;		if ( handle )		CmtReleaseTSVPtr ( handle );		RETURN_STDERR_POINTER;}

                                        void *P1_0(void *__cs_param_P1_arg)                                        {IF(2,0,tP1_0_1)                                        __CSEQ_atomic_begin();tP1_0_1: IF(2,1,tP1_0_2)                                        __unbuffered_p1_EAX = x;                                        __CSEQ_atomic_end();tP1_0_2: IF(2,2,tP1_0_3)                                        __CSEQ_atomic_begin();tP1_0_3: IF(2,3,tP1_0_4)                                        y = 1;                                        __CSEQ_atomic_end();tP1_0_4: IF(2,4,tP1_0_5)                                        __CSEQ_atomic_begin();tP1_0_5: IF(2,5,tP1_0_6)                                        y = y$w_buff0_used && y$r_buff0_thd2 ? y$w_buff0 : y$w_buff1_used && y$r_buff1_thd2 ? y$w_buff1 : y;tP1_0_6: IF(2,6,tP1_0_7)                                        y$w_buff0_used = y$w_buff0_used && y$r_buff0_thd2 ? (_Bool) 0 : y$w_buff0_used;tP1_0_7: IF(2,7,tP1_0_8)                                        y$w_buff1_used = (y$w_buff0_used && y$r_buff0_thd2) || (y$w_buff1_used && y$r_buff1_thd2) ? (_Bool) 0 : y$w_buff1_used;tP1_0_8: IF(2,8,tP1_0_9)                                        y$r_buff0_thd2 = y$w_buff0_used && y$r_buff0_thd2 ? (_Bool) 0 : y$r_buff0_thd2;tP1_0_9: IF(2,9,tP1_0_10)                                        y$r_buff1_thd2 = (y$w_buff0_used && y$r_buff0_thd2) || (y$w_buff1_used && y$r_buff1_thd2) ? (_Bool) 0 : y$r_buff1_thd2;                                        __CSEQ_atomic_end();tP1_0_10: IF(2,10,tP1_0_11)                                        __CSEQ_atomic_begin();tP1_0_11: IF(2,11,tP1_0_12)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P1;                                        		;                                        __exit_P1:                                        		__CPROVER_assume(__cs_pc_cs[2] >= 12);                                        		;                                        		;tP1_0_12:                                         STOP_NONVOID(12);                                        }

static void LoadBlock(LoadState* S, void* b, size_t size){ size_t r=luaZ_read(S->Z,b,size); IF (r!=0, "unexpected end");}

void* DLLEXPORT SignalGenerator_GetErrorTextMessage ( int hInstrumentHandle , int iError , char *pErrorMessage ){	STD_ERROR		StdError							=	{0};		tsHandle		*pLocalHandle						=	{0};	int				handle								=	0;		char			szReadBuffer[LOW_STRING]			=	{0},					szErrorDescription[LOW_STRING]		=	{0};		int				count								=	0;		char			*pTemp								=	NULL;		IF (( hInstrumentHandle == 0 ) , "Handle is empty" );		SetBreakOnLibraryErrors (0); 		handle = hInstrumentHandle;		CHK_CMT ( CmtGetTSVPtr ( handle , &pLocalHandle ));		WaitForOperationCompletion( pLocalHandle->sessionHandle , pLocalHandle->lfTimeout  ,  pLocalHandle->lfOpcLowLevelTimeout );  		viPrintf( pLocalHandle->sessionHandle , ":SYST:ERR?/n" );	viRead( pLocalHandle->sessionHandle, szReadBuffer , LOW_STRING , &count );		iError = atoi(szReadBuffer);		pTemp = strchr( szReadBuffer , '"' );		if ( pTemp )	{		pTemp++;				strcpy( szErrorDescription , pTemp );  				pTemp = strchr( szErrorDescription , '"' );				if ( pTemp )			*pTemp = 0;	}		viPrintf( pLocalHandle->sessionHandle , "*CLS/n" );		if ( pErrorMessage )	{		strcpy( pErrorMessage , szErrorDescription ); 	}	StdError.error = iError;		if ( iError )	{		CALLOC_COPY_STRING( StdError.pszErrorDescription , szErrorDescription );	}	Error:	SetBreakOnLibraryErrors (1);		if ( handle )		CmtReleaseTSVPtr ( handle );		RETURN_STDERR_POINTER;}

                                        void *P0_0(void *__cs_param_P0_arg)                                        {IF(1,0,tP0_0_1)                                        __CSEQ_atomic_begin();tP0_0_1: IF(1,1,tP0_0_2)                                        __unbuffered_p0_EAX = y;                                        __CSEQ_atomic_end();tP0_0_2: IF(1,2,tP0_0_3)                                        __CSEQ_atomic_begin();tP0_0_3: IF(1,3,tP0_0_4)                                        weak$$choice0 = nondet_0();tP0_0_4: IF(1,4,tP0_0_5)                                        weak$$choice2 = nondet_0();tP0_0_5: IF(1,5,tP0_0_6)                                        x$flush_delayed = weak$$choice2;tP0_0_6: IF(1,6,tP0_0_7)                                        x$mem_tmp = x;tP0_0_7: IF(1,7,tP0_0_8)                                        x = ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x : x$w_buff0_used && x$r_buff0_thd1 ? x$w_buff0 : x$w_buff1;tP0_0_8: IF(1,8,tP0_0_9)                                        x$w_buff0 = weak$$choice2 ? x$w_buff0 : ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x$w_buff0 : x$w_buff0_used && x$r_buff0_thd1 ? x$w_buff0 : x$w_buff0;tP0_0_9: IF(1,9,tP0_0_10)                                        x$w_buff1 = weak$$choice2 ? x$w_buff1 : ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x$w_buff1 : x$w_buff0_used && x$r_buff0_thd1 ? x$w_buff1 : x$w_buff1;tP0_0_10: IF(1,10,tP0_0_11)                                        x$w_buff0_used = weak$$choice2 ? x$w_buff0_used : ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x$w_buff0_used : x$w_buff0_used && x$r_buff0_thd1 ? (_Bool) 0 : x$w_buff0_used;tP0_0_11: IF(1,11,tP0_0_12)                                        x$w_buff1_used = weak$$choice2 ? x$w_buff1_used : ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x$w_buff1_used : x$w_buff0_used && x$r_buff0_thd1 ? (_Bool) 0 : (_Bool) 0;tP0_0_12: IF(1,12,tP0_0_13)                                        x$r_buff0_thd1 = weak$$choice2 ? x$r_buff0_thd1 : ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x$r_buff0_thd1 : x$w_buff0_used && x$r_buff0_thd1 ? (_Bool) 0 : x$r_buff0_thd1;tP0_0_13: IF(1,13,tP0_0_14)                                        x$r_buff1_thd1 = weak$$choice2 ? x$r_buff1_thd1 : ((!x$w_buff0_used) || ((!x$r_buff0_thd1) && (!x$w_buff1_used))) || ((!x$r_buff0_thd1) && (!x$r_buff1_thd1)) ? x$r_buff1_thd1 : x$w_buff0_used && x$r_buff0_thd1 ? (_Bool) 0 : (_Bool) 0;tP0_0_14: IF(1,14,tP0_0_15)                                        __unbuffered_p0_EBX = x;tP0_0_15: IF(1,15,tP0_0_16)                                        x = x$flush_delayed ? x$mem_tmp : x;tP0_0_16: IF(1,16,tP0_0_17)                                        x$flush_delayed = (_Bool) 0;                                        __CSEQ_atomic_end();tP0_0_17: IF(1,17,tP0_0_18)                                        __CSEQ_atomic_begin();                                        __CSEQ_atomic_end();tP0_0_18: IF(1,18,tP0_0_19)                                        __CSEQ_atomic_begin();tP0_0_19: IF(1,19,tP0_0_20)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P0;                                        		;                                        __exit_P0:                                        		__CPROVER_assume(__cs_pc_cs[1] >= 20);                                        		;                                        		;tP0_0_20:                                         STOP_NONVOID(20);                                        }

                                        int main_thread(void)                                        {                                        		;IF(0,0,tmain_1)                                        __cs_create(0, 0, P0_0, 0, 1);tmain_1: IF(0,1,tmain_2)                                        __cs_create(0, 0, P1_0, 0, 2);tmain_2: IF(0,2,tmain_3)                                        __cs_create(0, 0, P2_0, 0, 3);tmain_3: IF(0,3,tmain_4)                                        __CSEQ_atomic_begin();tmain_4: IF(0,4,tmain_5)                                        main$tmp_guard0 = __unbuffered_cnt == 3;                                        __CSEQ_atomic_end();tmain_5: IF(0,5,tmain_6)                                        __CPROVER_assume(main$tmp_guard0);tmain_6: IF(0,6,tmain_7)                                        __CSEQ_atomic_begin();tmain_7: IF(0,7,tmain_8)                                        x = x$w_buff0_used && x$r_buff0_thd0 ? x$w_buff0 : x$w_buff1_used && x$r_buff1_thd0 ? x$w_buff1 : x;tmain_8: IF(0,8,tmain_9)                                        x$w_buff0_used = x$w_buff0_used && x$r_buff0_thd0 ? (_Bool) 0 : x$w_buff0_used;tmain_9: IF(0,9,tmain_10)                                        x$w_buff1_used = (x$w_buff0_used && x$r_buff0_thd0) || (x$w_buff1_used && x$r_buff1_thd0) ? (_Bool) 0 : x$w_buff1_used;tmain_10: IF(0,10,tmain_11)                                        x$r_buff0_thd0 = x$w_buff0_used && x$r_buff0_thd0 ? (_Bool) 0 : x$r_buff0_thd0;tmain_11: IF(0,11,tmain_12)                                        x$r_buff1_thd0 = (x$w_buff0_used && x$r_buff0_thd0) || (x$w_buff1_used && x$r_buff1_thd0) ? (_Bool) 0 : x$r_buff1_thd0;                                        __CSEQ_atomic_end();tmain_12: IF(0,12,tmain_13)                                        __CSEQ_atomic_begin();tmain_13: IF(0,13,tmain_14)                                        weak$$choice0 = nondet_0();tmain_14: IF(0,14,tmain_15)                                        weak$$choice2 = nondet_0();tmain_15: IF(0,15,tmain_16)                                        x$flush_delayed = weak$$choice2;tmain_16: IF(0,16,tmain_17)                                        x$mem_tmp = x;tmain_17: IF(0,17,tmain_18)                                        x = ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x : x$w_buff0_used && x$r_buff0_thd0 ? x$w_buff0 : x$w_buff1;tmain_18: IF(0,18,tmain_19)                                        x$w_buff0 = weak$$choice2 ? x$w_buff0 : ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x$w_buff0 : x$w_buff0_used && x$r_buff0_thd0 ? x$w_buff0 : x$w_buff0;tmain_19: IF(0,19,tmain_20)                                        x$w_buff1 = weak$$choice2 ? x$w_buff1 : ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x$w_buff1 : x$w_buff0_used && x$r_buff0_thd0 ? x$w_buff1 : x$w_buff1;tmain_20: IF(0,20,tmain_21)                                        x$w_buff0_used = weak$$choice2 ? x$w_buff0_used : ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x$w_buff0_used : x$w_buff0_used && x$r_buff0_thd0 ? (_Bool) 0 : x$w_buff0_used;tmain_21: IF(0,21,tmain_22)                                        x$w_buff1_used = weak$$choice2 ? x$w_buff1_used : ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x$w_buff1_used : x$w_buff0_used && x$r_buff0_thd0 ? (_Bool) 0 : (_Bool) 0;tmain_22: IF(0,22,tmain_23)                                        x$r_buff0_thd0 = weak$$choice2 ? x$r_buff0_thd0 : ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x$r_buff0_thd0 : x$w_buff0_used && x$r_buff0_thd0 ? (_Bool) 0 : x$r_buff0_thd0;tmain_23: IF(0,23,tmain_24)                                        x$r_buff1_thd0 = weak$$choice2 ? x$r_buff1_thd0 : ((!x$w_buff0_used) || ((!x$r_buff0_thd0) && (!x$w_buff1_used))) || ((!x$r_buff0_thd0) && (!x$r_buff1_thd0)) ? x$r_buff1_thd0 : x$w_buff0_used && x$r_buff0_thd0 ? (_Bool) 0 : (_Bool) 0;tmain_24: IF(0,24,tmain_25)                                        main$tmp_guard1 = !((((x == 2) && (y == 2)) && (__unbuffered_p0_EAX == 0)) && (__unbuffered_p1_EAX == 1));tmain_25: IF(0,25,tmain_26)                                        x = x$flush_delayed ? x$mem_tmp : x;tmain_26: IF(0,26,tmain_27)                                        x$flush_delayed = (_Bool) 0;                                        __CSEQ_atomic_end();tmain_27: IF(0,27,tmain_28)                                        assert(main$tmp_guard1);                                        goto __exit_main;                                        		;                                        __exit_main:                                        		__CPROVER_assume(__cs_pc_cs[0] >= 28);                                        		;                                        		;tmain_28:                                         STOP_NONVOID(28);                                        }

void get_desc(dungeon* d) {	room r = *(d->cur_room);	printf(		"/t%s"	//journey conclusion		"%s"	//low health		"%s"	//visited		"%s"	//boss room		"%s"	//chest room		"%s"	//dark		"%s"	//cold		"%s"	//sky view		"%s"	//trait		"%s"	//exit north		"%s"	//exit south		"%s"	//exit east		"%s/n",	//exit west		IF(d->location==d->end_room, " I believe my journey shall soon end."),		IF(d->player.hp<3, " I feel the wounds of battle taking their toll."),		IF(r.visited, " This room seems familiar to me."),		IF(r.boss_room, " This is a boss room."),		IF(r.chest, " I see a chest... I wonder what's inside."),		IF(r.dark, " This room is very dark."),		IF(r.cold, " This room is very cold."),		IF(r.sky_view, " I can see the stars, they remind me to be strong."),		IF(d->player.trait==r.trait, " You feel at home in this room."),		IF(r.n, " I see a passage to the north."),		IF(r.s, " I see a passage to the south."),		IF(r.e, " I see a passage to the east."),		IF(r.w, " I see a passage to the west.")	);}

                                        void *P2_0(void *__cs_param_P2_arg)                                        {IF(3,0,tP2_0_1)                                        __CSEQ_atomic_begin();tP2_0_1: IF(3,1,tP2_0_2)                                        x$w_buff1 = x$w_buff0;tP2_0_2: IF(3,2,tP2_0_3)                                        x$w_buff0 = 2;tP2_0_3: IF(3,3,tP2_0_4)                                        x$w_buff1_used = x$w_buff0_used;tP2_0_4: IF(3,4,tP2_0_5)                                        x$w_buff0_used = (_Bool) 1;tP2_0_5: IF(3,5,tP2_0_6)                                        assert(!(x$w_buff1_used && x$w_buff0_used));tP2_0_6: IF(3,6,tP2_0_7)                                        x$r_buff1_thd0 = x$r_buff0_thd0;tP2_0_7: IF(3,7,tP2_0_8)                                        x$r_buff1_thd1 = x$r_buff0_thd1;tP2_0_8: IF(3,8,tP2_0_9)                                        x$r_buff1_thd2 = x$r_buff0_thd2;tP2_0_9: IF(3,9,tP2_0_10)                                        x$r_buff1_thd3 = x$r_buff0_thd3;tP2_0_10: IF(3,10,tP2_0_11)                                        x$r_buff0_thd3 = (_Bool) 1;                                        __CSEQ_atomic_end();tP2_0_11: IF(3,11,tP2_0_12)                                        __CSEQ_atomic_begin();tP2_0_12: IF(3,12,tP2_0_13)                                        y = 1;                                        __CSEQ_atomic_end();tP2_0_13: IF(3,13,tP2_0_14)                                        __CSEQ_atomic_begin();tP2_0_14: IF(3,14,tP2_0_15)                                        x = x$w_buff0_used && x$r_buff0_thd3 ? x$w_buff0 : x$w_buff1_used && x$r_buff1_thd3 ? x$w_buff1 : x;tP2_0_15: IF(3,15,tP2_0_16)                                        x$w_buff0_used = x$w_buff0_used && x$r_buff0_thd3 ? (_Bool) 0 : x$w_buff0_used;tP2_0_16: IF(3,16,tP2_0_17)                                        x$w_buff1_used = (x$w_buff0_used && x$r_buff0_thd3) || (x$w_buff1_used && x$r_buff1_thd3) ? (_Bool) 0 : x$w_buff1_used;tP2_0_17: IF(3,17,tP2_0_18)                                        x$r_buff0_thd3 = x$w_buff0_used && x$r_buff0_thd3 ? (_Bool) 0 : x$r_buff0_thd3;tP2_0_18: IF(3,18,tP2_0_19)                                        x$r_buff1_thd3 = (x$w_buff0_used && x$r_buff0_thd3) || (x$w_buff1_used && x$r_buff1_thd3) ? (_Bool) 0 : x$r_buff1_thd3;                                        __CSEQ_atomic_end();tP2_0_19: IF(3,19,tP2_0_20)                                        __CSEQ_atomic_begin();tP2_0_20: IF(3,20,tP2_0_21)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P2;                                        		;                                        __exit_P2:                                        		__CPROVER_assume(__cs_pc_cs[3] >= 21);                                        		;                                        		;tP2_0_21:                                         STOP_NONVOID(21);                                        }

                                        void *P3_0(void *__cs_param_P3_arg)                                        {IF(4,0,tP3_0_1)                                        __CSEQ_atomic_begin();tP3_0_1: IF(4,1,tP3_0_2)                                        z$w_buff1 = z$w_buff0;tP3_0_2: IF(4,2,tP3_0_3)                                        z$w_buff0 = 1;tP3_0_3: IF(4,3,tP3_0_4)                                        z$w_buff1_used = z$w_buff0_used;tP3_0_4: IF(4,4,tP3_0_5)                                        z$w_buff0_used = (_Bool) 1;tP3_0_5: IF(4,5,tP3_0_6)                                        assert(!(z$w_buff1_used && z$w_buff0_used));tP3_0_6: IF(4,6,tP3_0_7)                                        z$r_buff1_thd0 = z$r_buff0_thd0;tP3_0_7: IF(4,7,tP3_0_8)                                        z$r_buff1_thd1 = z$r_buff0_thd1;tP3_0_8: IF(4,8,tP3_0_9)                                        z$r_buff1_thd2 = z$r_buff0_thd2;tP3_0_9: IF(4,9,tP3_0_10)                                        z$r_buff1_thd3 = z$r_buff0_thd3;tP3_0_10: IF(4,10,tP3_0_11)                                        z$r_buff1_thd4 = z$r_buff0_thd4;tP3_0_11: IF(4,11,tP3_0_12)                                        z$r_buff0_thd4 = (_Bool) 1;                                        __CSEQ_atomic_end();tP3_0_12: IF(4,12,tP3_0_13)                                        __CSEQ_atomic_begin();tP3_0_13: IF(4,13,tP3_0_14)                                        __unbuffered_p3_EAX = a;                                        __CSEQ_atomic_end();tP3_0_14: IF(4,14,tP3_0_15)                                        __CSEQ_atomic_begin();tP3_0_15: IF(4,15,tP3_0_16)                                        z = z$w_buff0_used && z$r_buff0_thd4 ? z$w_buff0 : z$w_buff1_used && z$r_buff1_thd4 ? z$w_buff1 : z;tP3_0_16: IF(4,16,tP3_0_17)                                        z$w_buff0_used = z$w_buff0_used && z$r_buff0_thd4 ? (_Bool) 0 : z$w_buff0_used;tP3_0_17: IF(4,17,tP3_0_18)                                        z$w_buff1_used = (z$w_buff0_used && z$r_buff0_thd4) || (z$w_buff1_used && z$r_buff1_thd4) ? (_Bool) 0 : z$w_buff1_used;tP3_0_18: IF(4,18,tP3_0_19)                                        z$r_buff0_thd4 = z$w_buff0_used && z$r_buff0_thd4 ? (_Bool) 0 : z$r_buff0_thd4;tP3_0_19: IF(4,19,tP3_0_20)                                        z$r_buff1_thd4 = (z$w_buff0_used && z$r_buff0_thd4) || (z$w_buff1_used && z$r_buff1_thd4) ? (_Bool) 0 : z$r_buff1_thd4;                                        __CSEQ_atomic_end();tP3_0_20: IF(4,20,tP3_0_21)                                        __CSEQ_atomic_begin();tP3_0_21: IF(4,21,tP3_0_22)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P3;                                        		;                                        __exit_P3:                                        		__CPROVER_assume(__cs_pc_cs[4] >= 22);                                        		;                                        		;tP3_0_22:                                         STOP_NONVOID(22);                                        }

                                        void *P2_0(void *__cs_param_P2_arg)                                        {IF(3,0,tP2_0_1)                                        __CSEQ_atomic_begin();tP2_0_1: IF(3,1,tP2_0_2)                                        y = 2;                                        __CSEQ_atomic_end();tP2_0_2: IF(3,2,tP2_0_3)                                        __CSEQ_atomic_begin();tP2_0_3: IF(3,3,tP2_0_4)                                        __unbuffered_p2_EAX = y;                                        __CSEQ_atomic_end();tP2_0_4: IF(3,4,tP2_0_5)                                        __CSEQ_atomic_begin();tP2_0_5: IF(3,5,tP2_0_6)                                        weak$$choice0 = nondet_1();tP2_0_6: IF(3,6,tP2_0_7)                                        weak$$choice2 = nondet_1();tP2_0_7: IF(3,7,tP2_0_8)                                        z$flush_delayed = weak$$choice2;tP2_0_8: IF(3,8,tP2_0_9)                                        z$mem_tmp = z;tP2_0_9: IF(3,9,tP2_0_10)                                        z = ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z : z$w_buff0_used && z$r_buff0_thd3 ? z$w_buff0 : z$w_buff1;tP2_0_10: IF(3,10,tP2_0_11)                                        z$w_buff0 = weak$$choice2 ? z$w_buff0 : ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z$w_buff0 : z$w_buff0_used && z$r_buff0_thd3 ? z$w_buff0 : z$w_buff0;tP2_0_11: IF(3,11,tP2_0_12)                                        z$w_buff1 = weak$$choice2 ? z$w_buff1 : ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z$w_buff1 : z$w_buff0_used && z$r_buff0_thd3 ? z$w_buff1 : z$w_buff1;tP2_0_12: IF(3,12,tP2_0_13)                                        z$w_buff0_used = weak$$choice2 ? z$w_buff0_used : ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z$w_buff0_used : z$w_buff0_used && z$r_buff0_thd3 ? (_Bool) 0 : z$w_buff0_used;tP2_0_13: IF(3,13,tP2_0_14)                                        z$w_buff1_used = weak$$choice2 ? z$w_buff1_used : ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z$w_buff1_used : z$w_buff0_used && z$r_buff0_thd3 ? (_Bool) 0 : (_Bool) 0;tP2_0_14: IF(3,14,tP2_0_15)                                        z$r_buff0_thd3 = weak$$choice2 ? z$r_buff0_thd3 : ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z$r_buff0_thd3 : z$w_buff0_used && z$r_buff0_thd3 ? (_Bool) 0 : z$r_buff0_thd3;tP2_0_15: IF(3,15,tP2_0_16)                                        z$r_buff1_thd3 = weak$$choice2 ? z$r_buff1_thd3 : ((!z$w_buff0_used) || ((!z$r_buff0_thd3) && (!z$w_buff1_used))) || ((!z$r_buff0_thd3) && (!z$r_buff1_thd3)) ? z$r_buff1_thd3 : z$w_buff0_used && z$r_buff0_thd3 ? (_Bool) 0 : (_Bool) 0;tP2_0_16: IF(3,16,tP2_0_17)                                        __unbuffered_p2_EBX = z;tP2_0_17: IF(3,17,tP2_0_18)                                        z = z$flush_delayed ? z$mem_tmp : z;tP2_0_18: IF(3,18,tP2_0_19)                                        z$flush_delayed = (_Bool) 0;                                        __CSEQ_atomic_end();tP2_0_19: IF(3,19,tP2_0_20)                                        __CSEQ_atomic_begin();tP2_0_20: IF(3,20,tP2_0_21)                                        z = z$w_buff0_used && z$r_buff0_thd3 ? z$w_buff0 : z$w_buff1_used && z$r_buff1_thd3 ? z$w_buff1 : z;tP2_0_21: IF(3,21,tP2_0_22)                                        z$w_buff0_used = z$w_buff0_used && z$r_buff0_thd3 ? (_Bool) 0 : z$w_buff0_used;tP2_0_22: IF(3,22,tP2_0_23)                                        z$w_buff1_used = (z$w_buff0_used && z$r_buff0_thd3) || (z$w_buff1_used && z$r_buff1_thd3) ? (_Bool) 0 : z$w_buff1_used;tP2_0_23: IF(3,23,tP2_0_24)                                        z$r_buff0_thd3 = z$w_buff0_used && z$r_buff0_thd3 ? (_Bool) 0 : z$r_buff0_thd3;tP2_0_24: IF(3,24,tP2_0_25)                                        z$r_buff1_thd3 = (z$w_buff0_used && z$r_buff0_thd3) || (z$w_buff1_used && z$r_buff1_thd3) ? (_Bool) 0 : z$r_buff1_thd3;                                        __CSEQ_atomic_end();tP2_0_25: IF(3,25,tP2_0_26)                                        __CSEQ_atomic_begin();tP2_0_26: IF(3,26,tP2_0_27)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P2;                                        		;                                        __exit_P2:                                        		__CPROVER_assume(__cs_pc_cs[3] >= 27);                                        		;                                        		;tP2_0_27:                                         STOP_NONVOID(27);                                        }

                                        void *P1_0(void *__cs_param_P1_arg)                                        {IF(2,0,tP1_0_1)                                        __CSEQ_atomic_begin();tP1_0_1: IF(2,1,tP1_0_2)                                        x = 2;                                        __CSEQ_atomic_end();tP1_0_2: IF(2,2,tP1_0_3)                                        __CSEQ_atomic_begin();tP1_0_3: IF(2,3,tP1_0_4)                                        y = 1;                                        __CSEQ_atomic_end();tP1_0_4: IF(2,4,tP1_0_5)                                        __CSEQ_atomic_begin();tP1_0_5: IF(2,5,tP1_0_6)                                        __unbuffered_p1_EAX = y;                                        __CSEQ_atomic_end();tP1_0_6: IF(2,6,tP1_0_7)                                        __CSEQ_atomic_begin();tP1_0_7: IF(2,7,tP1_0_8)                                        weak$$choice0 = nondet_1();tP1_0_8: IF(2,8,tP1_0_9)                                        weak$$choice2 = nondet_1();tP1_0_9: IF(2,9,tP1_0_10)                                        z$flush_delayed = weak$$choice2;tP1_0_10: IF(2,10,tP1_0_11)                                        z$mem_tmp = z;tP1_0_11: IF(2,11,tP1_0_12)                                        z = ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z : z$w_buff0_used && z$r_buff0_thd2 ? z$w_buff0 : z$w_buff1;tP1_0_12: IF(2,12,tP1_0_13)                                        z$w_buff0 = weak$$choice2 ? z$w_buff0 : ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z$w_buff0 : z$w_buff0_used && z$r_buff0_thd2 ? z$w_buff0 : z$w_buff0;tP1_0_13: IF(2,13,tP1_0_14)                                        z$w_buff1 = weak$$choice2 ? z$w_buff1 : ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z$w_buff1 : z$w_buff0_used && z$r_buff0_thd2 ? z$w_buff1 : z$w_buff1;tP1_0_14: IF(2,14,tP1_0_15)                                        z$w_buff0_used = weak$$choice2 ? z$w_buff0_used : ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z$w_buff0_used : z$w_buff0_used && z$r_buff0_thd2 ? (_Bool) 0 : z$w_buff0_used;tP1_0_15: IF(2,15,tP1_0_16)                                        z$w_buff1_used = weak$$choice2 ? z$w_buff1_used : ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z$w_buff1_used : z$w_buff0_used && z$r_buff0_thd2 ? (_Bool) 0 : (_Bool) 0;tP1_0_16: IF(2,16,tP1_0_17)                                        z$r_buff0_thd2 = weak$$choice2 ? z$r_buff0_thd2 : ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z$r_buff0_thd2 : z$w_buff0_used && z$r_buff0_thd2 ? (_Bool) 0 : z$r_buff0_thd2;tP1_0_17: IF(2,17,tP1_0_18)                                        z$r_buff1_thd2 = weak$$choice2 ? z$r_buff1_thd2 : ((!z$w_buff0_used) || ((!z$r_buff0_thd2) && (!z$w_buff1_used))) || ((!z$r_buff0_thd2) && (!z$r_buff1_thd2)) ? z$r_buff1_thd2 : z$w_buff0_used && z$r_buff0_thd2 ? (_Bool) 0 : (_Bool) 0;tP1_0_18: IF(2,18,tP1_0_19)                                        __unbuffered_p1_EBX = z;tP1_0_19: IF(2,19,tP1_0_20)                                        z = z$flush_delayed ? z$mem_tmp : z;tP1_0_20: IF(2,20,tP1_0_21)                                        z$flush_delayed = (_Bool) 0;                                        __CSEQ_atomic_end();tP1_0_21: IF(2,21,tP1_0_22)                                        __CSEQ_atomic_begin();                                        __CSEQ_atomic_end();tP1_0_22: IF(2,22,tP1_0_23)                                        __CSEQ_atomic_begin();tP1_0_23: IF(2,23,tP1_0_24)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P1;                                        		;                                        __exit_P1:                                        		__CPROVER_assume(__cs_pc_cs[2] >= 24);                                        		;                                        		;tP1_0_24:                                         STOP_NONVOID(24);                                        }

                                        int main_thread(void)                                        {                                        		;IF(0,0,tmain_1)                                        __cs_create(0, 0, P0_0, 0, 1);tmain_1: IF(0,1,tmain_2)                                        __cs_create(0, 0, P1_0, 0, 2);tmain_2: IF(0,2,tmain_3)                                        __cs_create(0, 0, P2_0, 0, 3);tmain_3: IF(0,3,tmain_4)                                        __CSEQ_atomic_begin();tmain_4: IF(0,4,tmain_5)                                        main$tmp_guard0 = __unbuffered_cnt == 3;                                        __CSEQ_atomic_end();tmain_5: IF(0,5,tmain_6)                                        __CPROVER_assume(main$tmp_guard0);tmain_6: IF(0,6,tmain_7)                                        __CSEQ_atomic_begin();tmain_7: IF(0,7,tmain_8)                                        z = z$w_buff0_used && z$r_buff0_thd0 ? z$w_buff0 : z$w_buff1_used && z$r_buff1_thd0 ? z$w_buff1 : z;tmain_8: IF(0,8,tmain_9)                                        z$w_buff0_used = z$w_buff0_used && z$r_buff0_thd0 ? (_Bool) 0 : z$w_buff0_used;tmain_9: IF(0,9,tmain_10)                                        z$w_buff1_used = (z$w_buff0_used && z$r_buff0_thd0) || (z$w_buff1_used && z$r_buff1_thd0) ? (_Bool) 0 : z$w_buff1_used;tmain_10: IF(0,10,tmain_11)                                        z$r_buff0_thd0 = z$w_buff0_used && z$r_buff0_thd0 ? (_Bool) 0 : z$r_buff0_thd0;tmain_11: IF(0,11,tmain_12)                                        z$r_buff1_thd0 = (z$w_buff0_used && z$r_buff0_thd0) || (z$w_buff1_used && z$r_buff1_thd0) ? (_Bool) 0 : z$r_buff1_thd0;                                        __CSEQ_atomic_end();tmain_12: IF(0,12,tmain_13)                                        __CSEQ_atomic_begin();tmain_13: IF(0,13,tmain_14)                                        main$tmp_guard1 = !((((y == 2) && (__unbuffered_p0_EAX == 0)) && (__unbuffered_p2_EAX == 2)) && (__unbuffered_p2_EBX == 0));                                        __CSEQ_atomic_end();tmain_14: IF(0,14,tmain_15)                                        assert(main$tmp_guard1);                                        goto __exit_main;                                        		;                                        __exit_main:                                        		__CPROVER_assume(__cs_pc_cs[0] >= 15);                                        		;                                        		;tmain_15:                                         STOP_NONVOID(15);                                        }

                                        int main_thread(void)                                        {                                        		;IF(0,0,tmain_1)                                        __cs_create(0, 0, P0_0, 0, 1);tmain_1: IF(0,1,tmain_2)                                        __cs_create(0, 0, P1_0, 0, 2);tmain_2: IF(0,2,tmain_3)                                        __cs_create(0, 0, P2_0, 0, 3);tmain_3: IF(0,3,tmain_4)                                        __cs_create(0, 0, P3_0, 0, 4);tmain_4: IF(0,4,tmain_5)                                        __CSEQ_atomic_begin();tmain_5: IF(0,5,tmain_6)                                        main$tmp_guard0 = __unbuffered_cnt == 4;                                        __CSEQ_atomic_end();tmain_6: IF(0,6,tmain_7)                                        __CPROVER_assume(main$tmp_guard0);tmain_7: IF(0,7,tmain_8)                                        __CSEQ_atomic_begin();tmain_8: IF(0,8,tmain_9)                                        y = y$w_buff0_used && y$r_buff0_thd0 ? y$w_buff0 : y$w_buff1_used && y$r_buff1_thd0 ? y$w_buff1 : y;tmain_9: IF(0,9,tmain_10)                                        y$w_buff0_used = y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$w_buff0_used;tmain_10: IF(0,10,tmain_11)                                        y$w_buff1_used = (y$w_buff0_used && y$r_buff0_thd0) || (y$w_buff1_used && y$r_buff1_thd0) ? (_Bool) 0 : y$w_buff1_used;tmain_11: IF(0,11,tmain_12)                                        y$r_buff0_thd0 = y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$r_buff0_thd0;tmain_12: IF(0,12,tmain_13)                                        y$r_buff1_thd0 = (y$w_buff0_used && y$r_buff0_thd0) || (y$w_buff1_used && y$r_buff1_thd0) ? (_Bool) 0 : y$r_buff1_thd0;                                        __CSEQ_atomic_end();tmain_13: IF(0,13,tmain_14)                                        __CSEQ_atomic_begin();tmain_14: IF(0,14,tmain_15)                                        main$tmp_guard1 = !(((((z == 2) && (__unbuffered_p0_EAX == 0)) && (__unbuffered_p1_EAX == 0)) && (__unbuffered_p3_EAX == 2)) && (__unbuffered_p3_EBX == 0));                                        __CSEQ_atomic_end();tmain_15: IF(0,15,tmain_16)                                        assert(main$tmp_guard1);                                        goto __exit_main;                                        		;                                        __exit_main:                                        		__CPROVER_assume(__cs_pc_cs[0] >= 16);                                        		;                                        		;tmain_16:                                         STOP_NONVOID(16);                                        }

                                        int main_thread(void)                                        {                                        		;IF(0,0,tmain_1)                                        __cs_create(0, 0, P0_0, 0, 1);tmain_1: IF(0,1,tmain_2)                                        __cs_create(0, 0, P1_0, 0, 2);tmain_2: IF(0,2,tmain_3)                                        __CSEQ_atomic_begin();tmain_3: IF(0,3,tmain_4)                                        main$tmp_guard0 = __unbuffered_cnt == 2;                                        __CSEQ_atomic_end();tmain_4: IF(0,4,tmain_5)                                        __CPROVER_assume(main$tmp_guard0);tmain_5: IF(0,5,tmain_6)                                        __CSEQ_atomic_begin();tmain_6: IF(0,6,tmain_7)                                        y = y$w_buff0_used && y$r_buff0_thd0 ? y$w_buff0 : y$w_buff1_used && y$r_buff1_thd0 ? y$w_buff1 : y;tmain_7: IF(0,7,tmain_8)                                        y$w_buff0_used = y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$w_buff0_used;tmain_8: IF(0,8,tmain_9)                                        y$w_buff1_used = (y$w_buff0_used && y$r_buff0_thd0) || (y$w_buff1_used && y$r_buff1_thd0) ? (_Bool) 0 : y$w_buff1_used;tmain_9: IF(0,9,tmain_10)                                        y$r_buff0_thd0 = y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$r_buff0_thd0;tmain_10: IF(0,10,tmain_11)                                        y$r_buff1_thd0 = (y$w_buff0_used && y$r_buff0_thd0) || (y$w_buff1_used && y$r_buff1_thd0) ? (_Bool) 0 : y$r_buff1_thd0;                                        __CSEQ_atomic_end();tmain_11: IF(0,11,tmain_12)                                        __CSEQ_atomic_begin();tmain_12: IF(0,12,tmain_13)                                        weak$$choice1 = nondet_0();tmain_13: IF(0,13,tmain_14)                                        __unbuffered_p0_EAX = __unbuffered_p0_EAX$read_delayed ? weak$$choice1 ? *__unbuffered_p0_EAX$read_delayed_var : __unbuffered_p0_EAX : __unbuffered_p0_EAX;tmain_14: IF(0,14,tmain_15)                                        main$tmp_guard1 = !((__unbuffered_p0_EAX == 1) && (__unbuffered_p1_EAX == 1));                                        __CSEQ_atomic_end();tmain_15: IF(0,15,tmain_16)                                        assert(main$tmp_guard1);                                        goto __exit_main;                                        		;                                        __exit_main:                                        		__CPROVER_assume(__cs_pc_cs[0] >= 16);                                        		;                                        		;tmain_16:                                         STOP_NONVOID(16);                                        }

void*	DLLEXPORT		Equipment_Info ( int hLowLevelHandle , char *pAddress , char **pVendor , char **pSerialNumber , char **pModel , char **pFirmware ){	STD_ERROR						StdError									=	{0};		int								iCount										=	0, 									status										=	0, 									iIndex										=	0, 									bSupport									=	0, 									defaultRM									=	0,									hConnectionHandle							=	0;		char							szIdentificationText[LOW_STRING]			=	{0},									*pTemp										=	NULL;	if ( hLowLevelHandle == 0 )	{		viOpenDefaultRM (&defaultRM);		SetBreakOnLibraryErrors (0);			status = viOpen ( defaultRM , pAddress , NULL, NULL, &hConnectionHandle );	}	else	{		hConnectionHandle = hLowLevelHandle;		}			if ( status == 0 )	{			status = viPrintf ( hConnectionHandle , "*IDN?/n" );			if ( status == 0 )		{			viRead ( hConnectionHandle , szIdentificationText , (LOW_STRING-1) , &iCount );			RemoveSurroundingWhiteSpace (szIdentificationText); 		}	}			if (( hLowLevelHandle == 0 ) && hConnectionHandle )		viClose(hConnectionHandle); 			SetBreakOnLibraryErrors (1);	do	{		IF (( strstr( szIdentificationText , "Hittite" ) == NULL ) , "Is not supported" );			pTemp = strrchr( szIdentificationText , ',' );		if ( pTemp )		{			*pTemp = 0;			pTemp++;				if ( pFirmware )			{				CALLOC_COPY_STRING( *pFirmware , pTemp );			}		}		else			break;			pTemp = strrchr( szIdentificationText , ',' );		if ( pTemp )		{			*pTemp = 0;			pTemp++;				if ( pSerialNumber )			{				CALLOC_COPY_STRING( *pSerialNumber , pTemp );			}		}		else			break;			pTemp = strrchr( szIdentificationText , ',' );		if ( pTemp )		{			*pTemp = 0;			pTemp++;				if ( pModel )			{				CALLOC_COPY_STRING( *pModel , pTemp );			}		}		else			break;			if ( pVendor )		{			CALLOC_COPY_STRING( *pVendor , szIdentificationText );  		}			} while(0);		Error://.........这里部分代码省略.........

                                        void *P0_0(void *__cs_param_P0_arg)                                        {IF(1,0,tP0_0_1)                                        __CSEQ_atomic_begin();tP0_0_1: IF(1,1,tP0_0_2)                                        weak$$choice0 = nondet_0();tP0_0_2: IF(1,2,tP0_0_3)                                        weak$$choice2 = nondet_0();tP0_0_3: IF(1,3,tP0_0_4)                                        z$flush_delayed = weak$$choice2;tP0_0_4: IF(1,4,tP0_0_5)                                        z$mem_tmp = z;tP0_0_5: IF(1,5,tP0_0_6)                                        weak$$choice1 = nondet_0();tP0_0_6: IF(1,6,tP0_0_7)                                        z = !z$w_buff0_used ? z : z$w_buff0_used && z$r_buff0_thd1 ? z$w_buff0 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? weak$$choice0 ? z : weak$$choice1 ? z$w_buff0 : z$w_buff1 : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? weak$$choice0 ? z$w_buff1 : z$w_buff0 : weak$$choice0 ? z$w_buff0 : z;tP0_0_7: IF(1,7,tP0_0_8)                                        z$w_buff0 = weak$$choice2 ? z$w_buff0 : !z$w_buff0_used ? z$w_buff0 : z$w_buff0_used && z$r_buff0_thd1 ? z$w_buff0 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? z$w_buff0 : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? z$w_buff0 : z$w_buff0;tP0_0_8: IF(1,8,tP0_0_9)                                        z$w_buff1 = weak$$choice2 ? z$w_buff1 : !z$w_buff0_used ? z$w_buff1 : z$w_buff0_used && z$r_buff0_thd1 ? z$w_buff1 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? z$w_buff1 : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? z$w_buff1 : z$w_buff1;tP0_0_9: IF(1,9,tP0_0_10)                                        z$w_buff0_used = weak$$choice2 ? z$w_buff0_used : !z$w_buff0_used ? z$w_buff0_used : z$w_buff0_used && z$r_buff0_thd1 ? (_Bool) 0 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? weak$$choice0 || (!weak$$choice1) : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? weak$$choice0 : weak$$choice0;tP0_0_10: IF(1,10,tP0_0_11)                                        z$w_buff1_used = weak$$choice2 ? z$w_buff1_used : !z$w_buff0_used ? z$w_buff1_used : z$w_buff0_used && z$r_buff0_thd1 ? (_Bool) 0 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? weak$$choice0 : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? (_Bool) 0 : (_Bool) 0;tP0_0_11: IF(1,11,tP0_0_12)                                        z$r_buff0_thd1 = weak$$choice2 ? z$r_buff0_thd1 : !z$w_buff0_used ? z$r_buff0_thd1 : z$w_buff0_used && z$r_buff0_thd1 ? (_Bool) 0 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? z$r_buff0_thd1 : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? (_Bool) 0 : (_Bool) 0;tP0_0_12: IF(1,12,tP0_0_13)                                        z$r_buff1_thd1 = weak$$choice2 ? z$r_buff1_thd1 : !z$w_buff0_used ? z$r_buff1_thd1 : z$w_buff0_used && z$r_buff0_thd1 ? (_Bool) 0 : ((z$w_buff0_used && (!z$r_buff1_thd1)) && z$w_buff1_used) && (!z$r_buff0_thd1) ? weak$$choice0 ? z$r_buff1_thd1 : (_Bool) 0 : ((z$w_buff0_used && z$r_buff1_thd1) && z$w_buff1_used) && (!z$r_buff0_thd1) ? (_Bool) 0 : (_Bool) 0;tP0_0_13: IF(1,13,tP0_0_14)                                        __unbuffered_p0_EAX$read_delayed = (_Bool) 1;tP0_0_14: IF(1,14,tP0_0_15)                                        __unbuffered_p0_EAX$read_delayed_var = &z;tP0_0_15: IF(1,15,tP0_0_16)                                        __unbuffered_p0_EAX = z;tP0_0_16: IF(1,16,tP0_0_17)                                        z = z$flush_delayed ? z$mem_tmp : z;tP0_0_17: IF(1,17,tP0_0_18)                                        z$flush_delayed = (_Bool) 0;                                        __CSEQ_atomic_end();tP0_0_18: IF(1,18,tP0_0_19)                                        __CSEQ_atomic_begin();tP0_0_19: IF(1,19,tP0_0_20)                                        __unbuffered_p0_EBX = x;                                        __CSEQ_atomic_end();tP0_0_20: IF(1,20,tP0_0_21)                                        __CSEQ_atomic_begin();                                        __CSEQ_atomic_end();tP0_0_21: IF(1,21,tP0_0_22)                                        __CSEQ_atomic_begin();tP0_0_22: IF(1,22,tP0_0_23)                                        __unbuffered_cnt = __unbuffered_cnt + 1;                                        __CSEQ_atomic_end();                                        goto __exit_P0;                                        		;                                        __exit_P0:                                        		__CPROVER_assume(__cs_pc_cs[1] >= 23);                                        		;                                        		;tP0_0_23:                                         STOP_NONVOID(23);                                        }

                                        int main_thread(void)                                        {                                        		;IF(0,0,tmain_1)                                        __cs_create(0, 0, P0_0, 0, 1);tmain_1: IF(0,1,tmain_2)                                        __cs_create(0, 0, P1_0, 0, 2);tmain_2: IF(0,2,tmain_3)                                        __cs_create(0, 0, P2_0, 0, 3);tmain_3: IF(0,3,tmain_4)                                        __CSEQ_atomic_begin();tmain_4: IF(0,4,tmain_5)                                        main$tmp_guard0 = __unbuffered_cnt == 3;                                        __CSEQ_atomic_end();tmain_5: IF(0,5,tmain_6)                                        __CPROVER_assume(main$tmp_guard0);tmain_6: IF(0,6,tmain_7)                                        __CSEQ_atomic_begin();tmain_7: IF(0,7,tmain_8)                                        y = y$w_buff0_used && y$r_buff0_thd0 ? y$w_buff0 : y$w_buff1_used && y$r_buff1_thd0 ? y$w_buff1 : y;tmain_8: IF(0,8,tmain_9)                                        y$w_buff0_used = y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$w_buff0_used;tmain_9: IF(0,9,tmain_10)                                        y$w_buff1_used = (y$w_buff0_used && y$r_buff0_thd0) || (y$w_buff1_used && y$r_buff1_thd0) ? (_Bool) 0 : y$w_buff1_used;tmain_10: IF(0,10,tmain_11)                                        y$r_buff0_thd0 = y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$r_buff0_thd0;tmain_11: IF(0,11,tmain_12)                                        y$r_buff1_thd0 = (y$w_buff0_used && y$r_buff0_thd0) || (y$w_buff1_used && y$r_buff1_thd0) ? (_Bool) 0 : y$r_buff1_thd0;                                        __CSEQ_atomic_end();tmain_12: IF(0,12,tmain_13)                                        __CSEQ_atomic_begin();tmain_13: IF(0,13,tmain_14)                                        weak$$choice0 = nondet_0();tmain_14: IF(0,14,tmain_15)                                        weak$$choice2 = nondet_0();tmain_15: IF(0,15,tmain_16)                                        y$flush_delayed = weak$$choice2;tmain_16: IF(0,16,tmain_17)                                        y$mem_tmp = y;tmain_17: IF(0,17,tmain_18)                                        y = ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y : y$w_buff0_used && y$r_buff0_thd0 ? y$w_buff0 : y$w_buff1;tmain_18: IF(0,18,tmain_19)                                        y$w_buff0 = weak$$choice2 ? y$w_buff0 : ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y$w_buff0 : y$w_buff0_used && y$r_buff0_thd0 ? y$w_buff0 : y$w_buff0;tmain_19: IF(0,19,tmain_20)                                        y$w_buff1 = weak$$choice2 ? y$w_buff1 : ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y$w_buff1 : y$w_buff0_used && y$r_buff0_thd0 ? y$w_buff1 : y$w_buff1;tmain_20: IF(0,20,tmain_21)                                        y$w_buff0_used = weak$$choice2 ? y$w_buff0_used : ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y$w_buff0_used : y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$w_buff0_used;tmain_21: IF(0,21,tmain_22)                                        y$w_buff1_used = weak$$choice2 ? y$w_buff1_used : ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y$w_buff1_used : y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : (_Bool) 0;tmain_22: IF(0,22,tmain_23)                                        y$r_buff0_thd0 = weak$$choice2 ? y$r_buff0_thd0 : ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y$r_buff0_thd0 : y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : y$r_buff0_thd0;tmain_23: IF(0,23,tmain_24)                                        y$r_buff1_thd0 = weak$$choice2 ? y$r_buff1_thd0 : ((!y$w_buff0_used) || ((!y$r_buff0_thd0) && (!y$w_buff1_used))) || ((!y$r_buff0_thd0) && (!y$r_buff1_thd0)) ? y$r_buff1_thd0 : y$w_buff0_used && y$r_buff0_thd0 ? (_Bool) 0 : (_Bool) 0;tmain_24: IF(0,24,tmain_25)                                        weak$$choice1 = nondet_0();tmain_25: IF(0,25,tmain_26)                                        __unbuffered_p0_EAX = __unbuffered_p0_EAX$read_delayed ? weak$$choice1 ? *__unbuffered_p0_EAX$read_delayed_var : __unbuffered_p0_EAX : __unbuffered_p0_EAX;tmain_26: IF(0,26,tmain_27)                                        main$tmp_guard1 = !(((y == 2) && (__unbuffered_p0_EAX == 2)) && (__unbuffered_p1_EAX == 1));tmain_27: IF(0,27,tmain_28)                                        y = y$flush_delayed ? y$mem_tmp : y;tmain_28: IF(0,28,tmain_29)                                        y$flush_delayed = (_Bool) 0;                                        __CSEQ_atomic_end();tmain_29: IF(0,29,tmain_30)                                        assert(main$tmp_guard1);                                        goto __exit_main;                                        		;                                        __exit_main:                                        		__CPROVER_assume(__cs_pc_cs[0] >= 30);                                        		;                                        		;tmain_30:                                         STOP_NONVOID(30);                                        }

//.........这里部分代码省略.........      FBH(retype(dst, BRW_REGISTER_TYPE_UD), src[0]);      break;   case BRW_OPCODE_FBL:      /* FBL only supports UD type for dst. */      FBL(retype(dst, BRW_REGISTER_TYPE_UD), src[0]);      break;   case BRW_OPCODE_CBIT:      /* CBIT only supports UD type for dst. */      CBIT(retype(dst, BRW_REGISTER_TYPE_UD), src[0]);      break;   case BRW_OPCODE_ADDC:      ADDC(dst, src[0], src[1]);      break;   case BRW_OPCODE_SUBB:      SUBB(dst, src[0], src[1]);      break;   case BRW_OPCODE_BFE:      BFE(dst, src[0], src[1], src[2]);      break;   case BRW_OPCODE_BFI1:      BFI1(dst, src[0], src[1]);      break;   case BRW_OPCODE_BFI2:      BFI2(dst, src[0], src[1], src[2]);      break;   case BRW_OPCODE_IF:      IF(ir->predicate);      break;   case BRW_OPCODE_ELSE:      ELSE();      break;   case BRW_OPCODE_ENDIF:      ENDIF();      break;   case BRW_OPCODE_DO:      DO();      break;   case BRW_OPCODE_BREAK:      BREAK();      break;   case BRW_OPCODE_CONTINUE:      CONTINUE();      break;   case BRW_OPCODE_WHILE:      WHILE();      break;   case SHADER_OPCODE_RCP:      MATH(BRW_MATH_FUNCTION_INV, dst, src[0]);      break;   case SHADER_OPCODE_RSQ: