FlexCAN_Ip_GetListenOnlyMode (uint8 instance) { const struct FLEXCAN_Type * base; int _1; boolean _6; : # DEBUG BEGIN_STMT _1 = (int) instance_2(D); base_4 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_4 # DEBUG BEGIN_STMT _6 = FlexCAN_IsListenOnlyModeEnabled (base_4); return _6; } FlexCAN_Ip_SetListenOnlyMode_Privileged (uint8 instance, const boolean enable) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _33; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_22 = (boolean) _7; # DEBUG disabled => disabled_22 # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_24 = FlexCAN_Enable (pBase_20); # DEBUG result => result_24 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_26 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_26 # DEBUG BEGIN_STMT _8 = ~freeze_26; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = 1; # DEBUG result => result_27 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetListenOnlyMode (pBase_20, enable_28(D)); : # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_31 = FlexCAN_Disable (pBase_20); # DEBUG status => status_31 # DEBUG BEGIN_STMT if (status_31 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_32 = status_31; # DEBUG result => result_32 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _33 = result_11; return _33; } FlexCAN_Ip_SetRxMb15Mask_Privileged (uint8 instance, uint32 mask) { boolean disabled; boolean freeze; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _34; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT freeze_21 = 0; # DEBUG freeze => freeze_21 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_23 = (boolean) _7; # DEBUG disabled => disabled_23 # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_25 = FlexCAN_Enable (pBase_20); # DEBUG result => result_25 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_27 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_27 # DEBUG BEGIN_STMT _8 = ~freeze_27; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_28 = 1; # DEBUG result => result_28 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_20->RX15MASK ={v} mask_29(D); : # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_32 = FlexCAN_Disable (pBase_20); # DEBUG status => status_32 # DEBUG BEGIN_STMT if (status_32 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_33 = status_32; # DEBUG result => result_33 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _34 = result_11; return _34; } FlexCAN_Ip_SetRxMb14Mask_Privileged (uint8 instance, uint32 mask) { boolean disabled; boolean freeze; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _34; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT freeze_21 = 0; # DEBUG freeze => freeze_21 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_23 = (boolean) _7; # DEBUG disabled => disabled_23 # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_25 = FlexCAN_Enable (pBase_20); # DEBUG result => result_25 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_27 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_27 # DEBUG BEGIN_STMT _8 = ~freeze_27; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_28 = 1; # DEBUG result => result_28 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_20->RX14MASK ={v} mask_29(D); : # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_32 = FlexCAN_Disable (pBase_20); # DEBUG status => status_32 # DEBUG BEGIN_STMT if (status_32 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_33 = status_32; # DEBUG result => result_33 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _34 = result_11; return _34; } FlexCAN_Ip_AbortTransfer (uint8 u8Instance, uint8 mb_idx) { Flexcan_Ip_StatusType result; const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * pBase; _Bool _1; unsigned char _2; _Bool _3; int _4; int _5; int _6; _7; long unsigned int _8; _Bool _9; int _10; _11; int _12; _13; Flexcan_Ip_StatusType _31; : # DEBUG BEGIN_STMT _1 = u8Instance_18(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = mb_idx_21(D) + 160; _3 = _2 > 158; DevAssert (_3); # DEBUG BEGIN_STMT _4 = (int) u8Instance_18(D); pBase_23 = g_Flexcan_Ip_aBase[_4]; # DEBUG pBase => pBase_23 # DEBUG BEGIN_STMT _5 = (int) u8Instance_18(D); state_24 = g_flexcan_Ip_StatePtr[_5]; # DEBUG state => state_24 # DEBUG BEGIN_STMT result_25 = 0; # DEBUG result => result_25 # DEBUG BEGIN_STMT if (mb_idx_21(D) <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = (int) mb_idx_21(D); _7 ={v} state_24->mbs[_6].state; if (_7 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_30 = 5; # DEBUG result => result_30 goto ; [INV] : # DEBUG BEGIN_STMT _8 = (long unsigned int) mb_idx_21(D); _9 = state_24->isIntActive; FLEXCAN_ClearMsgBuffIntCmd (pBase_23, u8Instance_18(D), _8, _9); # DEBUG BEGIN_STMT _10 = (int) mb_idx_21(D); _11 ={v} state_24->mbs[_10].state; if (_11 == 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_28 = FlexCAN_AbortTxTransfer (u8Instance_18(D), mb_idx_21(D)); # DEBUG result => result_28 : # result_14 = PHI # DEBUG result => result_14 # DEBUG BEGIN_STMT _12 = (int) mb_idx_21(D); _13 ={v} state_24->mbs[_12].state; if (_13 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_AbortRxTransfer (u8Instance_18(D), mb_idx_21(D)); : # result_15 = PHI # DEBUG result => result_15 # DEBUG BEGIN_STMT _31 = result_15; return _31; } FlexCAN_Ip_SetErrorInt_Privileged (uint8 u8Instance, Flexcan_Ip_ErrorIntType type, boolean enable) { boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; int _8; _Bool _9; _Bool _10; _Bool _11; _Bool _12; Flexcan_Ip_StatusType _44; : # DEBUG BEGIN_STMT _1 = u8Instance_19(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_22 = 0; # DEBUG result => result_22 # DEBUG BEGIN_STMT status_23 = 0; # DEBUG status => status_23 # DEBUG BEGIN_STMT _2 = (int) u8Instance_19(D); pBase_24 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_24 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_24); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_26 = (boolean) _7; # DEBUG disabled => disabled_26 # DEBUG BEGIN_STMT if (disabled_26 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_28 = FlexCAN_Enable (pBase_24); # DEBUG result => result_28 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT if (result_13 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = (int) type_29(D); switch (_8) [INV], case 0: [INV], case 1: [INV], case 2: [INV], case 3: [INV], case 4: [INV]> : : # DEBUG BEGIN_STMT FlexCAN_SetErrIntCmd (pBase_24, 32768, enable_30(D)); # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_SetErrIntCmd (pBase_24, 16384, enable_30(D)); # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_SetErrIntCmd (pBase_24, 16385, enable_30(D)); # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT _9 = FlexCAN_IsFreezeMode (pBase_24); _10 = ~_9; if (_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_39 = 1; # DEBUG result => result_39 goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetErrIntCmd (pBase_24, 1024, enable_30(D)); goto ; [INV] : : # DEBUG BEGIN_STMT _11 = FlexCAN_IsFreezeMode (pBase_24); _12 = ~_11; if (_12 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_36 = 1; # DEBUG result => result_36 goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetErrIntCmd (pBase_24, 2048, enable_30(D)); goto ; [INV] : : # DEBUG BEGIN_STMT DevAssert (0); # DEBUG BEGIN_STMT : # result_14 = PHI # DEBUG result => result_14 # DEBUG BEGIN_STMT if (disabled_26 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_42 = FlexCAN_Disable (pBase_24); # DEBUG status => status_42 # DEBUG BEGIN_STMT if (status_42 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_43 = status_42; # DEBUG result => result_43 : # result_15 = PHI # DEBUG result => result_15 # DEBUG BEGIN_STMT _44 = result_15; return _44; } FlexCAN_Ip_DisableInterrupts_Privileged (uint8 u8Instance) { struct Flexcan_Ip_StateType * state; Flexcan_Ip_StatusType result; struct FLEXCAN_Type * pBase; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; _Bool _6; Flexcan_Ip_StatusType _23; : # DEBUG BEGIN_STMT _1 = (int) u8Instance_10(D); pBase_12 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_12 # DEBUG BEGIN_STMT result_13 = 1; # DEBUG result => result_13 # DEBUG BEGIN_STMT _2 = (int) u8Instance_10(D); state_14 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_14 # DEBUG BEGIN_STMT _3 = u8Instance_10(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnabled (pBase_12); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_DisableInterrupts (pBase_12); # DEBUG BEGIN_STMT _5 = FlexCAN_IsEnhancedRxFifoAvailable (pBase_12); if (_5 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = FlexCAN_IsEnhancedRxFifoEnabled (pBase_12); if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedRxFifoIntAll (pBase_12, 0); : # DEBUG BEGIN_STMT state_14->isIntActive = 0; # DEBUG BEGIN_STMT result_22 = 0; # DEBUG result => result_22 : # result_7 = PHI # DEBUG result => result_7 # DEBUG BEGIN_STMT _23 = result_7; return _23; } FlexCAN_Ip_EnableInterrupts_Privileged (uint8 u8Instance) { struct Flexcan_Ip_StateType * state; Flexcan_Ip_StatusType result; struct FLEXCAN_Type * pBase; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; _Bool _6; _Bool _7; _Bool _8; Flexcan_Ip_StatusType _25; : # DEBUG BEGIN_STMT _1 = (int) u8Instance_12(D); pBase_14 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_14 # DEBUG BEGIN_STMT result_15 = 1; # DEBUG result => result_15 # DEBUG BEGIN_STMT _2 = (int) u8Instance_12(D); state_16 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_16 # DEBUG BEGIN_STMT _3 = u8Instance_12(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnabled (pBase_14); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_EnableInterrupts (pBase_14, u8Instance_12(D)); # DEBUG BEGIN_STMT _5 = state_16->enhancedFifoOutput.isPolling; _6 = ~_5; if (_6 != 0) goto ; [INV] else goto ; [INV] : _7 = FlexCAN_IsEnhancedRxFifoAvailable (pBase_14); if (_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = FlexCAN_IsEnhancedRxFifoEnabled (pBase_14); if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedRxFifoIntAll (pBase_14, 1); : # DEBUG BEGIN_STMT state_16->isIntActive = 1; # DEBUG BEGIN_STMT result_24 = 0; # DEBUG result => result_24 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT _25 = result_9; return _25; } FlexCAN_Ip_ClearBuffStatusFlag (uint8 instance, uint8 msgBuffIdx) { struct FLEXCAN_Type * pBase; _Bool _1; int _2; long unsigned int _3; : # DEBUG BEGIN_STMT _1 = instance_5(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) instance_5(D); pBase_8 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_8 # DEBUG BEGIN_STMT if (msgBuffIdx_9(D) == 255) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (pBase_8, 30); goto ; [INV] : # DEBUG BEGIN_STMT _3 = (long unsigned int) msgBuffIdx_9(D); FlexCAN_ClearMsgBuffIntStatusFlag (pBase_8, _3); : return; } FlexCAN_Ip_GetBuffStatusFlag (uint8 instance, uint8 msgBuffIdx) { const struct FLEXCAN_Type * pBase; boolean returnResult; _Bool _1; int _2; unsigned char _3; long unsigned int _4; unsigned char _5; boolean _18; : # DEBUG BEGIN_STMT returnResult_8 = 1; # DEBUG returnResult => returnResult_8 # DEBUG BEGIN_STMT _1 = instance_9(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) instance_9(D); pBase_12 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_12 # DEBUG BEGIN_STMT if (msgBuffIdx_13(D) == 255) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _3 = FlexCAN_GetEnhancedRxFIFOStatusFlag (pBase_12, 30); returnResult_17 = _3 == 1; # DEBUG returnResult => returnResult_17 goto ; [INV] : # DEBUG BEGIN_STMT _4 = (long unsigned int) msgBuffIdx_13(D); _5 = FlexCAN_GetBuffStatusFlag (pBase_12, _4); returnResult_15 = _5 == 1; # DEBUG returnResult => returnResult_15 : # returnResult_6 = PHI # DEBUG returnResult => returnResult_6 # DEBUG BEGIN_STMT _18 = returnResult_6; return _18; } FlexCAN_Ip_SetTxArbitrationStartDelay_Privileged (uint8 instance, uint8 value) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _35; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_22 = (boolean) _7; # DEBUG disabled => disabled_22 # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_24 = FlexCAN_Enable (pBase_20); # DEBUG result => result_24 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_26 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_26 # DEBUG BEGIN_STMT _8 = ~freeze_26; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = 1; # DEBUG result => result_27 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_17 (); # DEBUG BEGIN_STMT FlexCAN_SetTxArbitrationStartDelay (pBase_20, value_29(D)); # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_17 (); : # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_33 = FlexCAN_Disable (pBase_20); # DEBUG status => status_33 # DEBUG BEGIN_STMT if (status_33 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_34 = status_33; # DEBUG result => result_34 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _35 = result_11; return _35; } FlexCAN_Ip_SetTDCOffset_Privileged (uint8 instance, boolean enable, uint8 offset) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; long unsigned int _9; long unsigned int _10; Flexcan_Ip_StatusType _40; : # DEBUG BEGIN_STMT _1 = instance_18(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_21 = 0; # DEBUG result => result_21 # DEBUG BEGIN_STMT status_22 = 0; # DEBUG status => status_22 # DEBUG BEGIN_STMT _2 = (int) instance_18(D); pBase_23 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_23 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_23); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_25 = (boolean) _7; # DEBUG disabled => disabled_25 # DEBUG BEGIN_STMT if (disabled_25 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = FlexCAN_Enable (pBase_23); # DEBUG result => result_27 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT freeze_29 = FlexCAN_IsFreezeMode (pBase_23); # DEBUG freeze => freeze_29 # DEBUG BEGIN_STMT _8 = ~freeze_29; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_30 = 1; # DEBUG result => result_30 : # result_12 = PHI # DEBUG result => result_12 # DEBUG BEGIN_STMT if (result_12 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_16 (); # DEBUG BEGIN_STMT _9 ={v} pBase_23->CTRL2; _10 = _9 & 8192; if (_10 == 8192) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedTDCOffset (pBase_23, enable_32(D), offset_33(D)); goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetTDCOffset (pBase_23, enable_32(D), offset_33(D)); : # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_16 (); : # DEBUG BEGIN_STMT if (disabled_25 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_38 = FlexCAN_Disable (pBase_23); # DEBUG status => status_38 # DEBUG BEGIN_STMT if (status_38 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_39 = status_38; # DEBUG result => result_39 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT _40 = result_13; return _40; } FlexCAN_Ip_GetBitrateFD (uint8 instance, struct Flexcan_Ip_TimeSegmentType * bitrate) { boolean enhCbt; const struct FLEXCAN_Type * pBase; _Bool _1; _Bool _2; int _3; boolean _15; : # DEBUG BEGIN_STMT _1 = instance_5(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = bitrate_8(D) != 0B; DevAssert (_2); # DEBUG BEGIN_STMT _3 = (int) instance_5(D); pBase_10 = g_Flexcan_Ip_aBase[_3]; # DEBUG pBase => pBase_10 # DEBUG BEGIN_STMT enhCbt_12 = FlexCAN_IsEnhCbtEnabled (pBase_10); # DEBUG enhCbt => enhCbt_12 # DEBUG BEGIN_STMT if (enhCbt_12 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_GetEnhancedDataTimeSegments (pBase_10, bitrate_8(D)); goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_GetFDTimeSegments (pBase_10, bitrate_8(D)); : # DEBUG BEGIN_STMT _15 = enhCbt_12; return _15; } FlexCAN_Ip_SetBitrateCbt_Privileged (uint8 instance, const struct Flexcan_Ip_TimeSegmentType * bitrate, boolean bitRateSwitch) { boolean enhCbt; boolean freeze; boolean fd_enable; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; _Bool _2; int _3; _Bool _4; int _5; _Bool _6; _Bool _7; int _8; _Bool _9; _Bool _10; Flexcan_Ip_StatusType _46; : # DEBUG BEGIN_STMT _1 = instance_18(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = bitrate_21(D) != 0B; DevAssert (_2); # DEBUG BEGIN_STMT result_23 = 0; # DEBUG result => result_23 # DEBUG BEGIN_STMT status_24 = 0; # DEBUG status => status_24 # DEBUG BEGIN_STMT _3 = (int) instance_18(D); pBase_25 = g_Flexcan_Ip_aBase[_3]; # DEBUG pBase => pBase_25 # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnabled (pBase_25); _5 = (int) _4; _6 = _5 != 0; _7 = ~_6; _8 = (int) _7; disabled_27 = (boolean) _8; # DEBUG disabled => disabled_27 # DEBUG BEGIN_STMT fd_enable_29 = FlexCAN_IsFDEnabled (pBase_25); # DEBUG fd_enable => fd_enable_29 # DEBUG BEGIN_STMT if (disabled_27 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_31 = FlexCAN_Enable (pBase_25); # DEBUG result => result_31 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT freeze_33 = FlexCAN_IsFreezeMode (pBase_25); # DEBUG freeze => freeze_33 # DEBUG BEGIN_STMT _9 = ~fd_enable_29; if (_9 != 0) goto ; [INV] else goto ; [INV] : _10 = ~freeze_33; if (_10 != 0) goto ; [INV] else goto ; [INV] : if (result_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_34 = 1; # DEBUG result => result_34 : # result_12 = PHI # DEBUG result => result_12 # DEBUG BEGIN_STMT if (result_12 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT enhCbt_36 = FlexCAN_IsEnhCbtEnabled (pBase_25); # DEBUG enhCbt => enhCbt_36 # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_15 (); # DEBUG BEGIN_STMT FlexCAN_SetFDEnabled (pBase_25, fd_enable_29, bitRateSwitch_38(D)); # DEBUG BEGIN_STMT if (enhCbt_36 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedDataTimeSegments (pBase_25, bitrate_21(D)); goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetFDTimeSegments (pBase_25, bitrate_21(D)); : # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_15 (); : # DEBUG BEGIN_STMT if (disabled_27 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_44 = FlexCAN_Disable (pBase_25); # DEBUG status => status_44 # DEBUG BEGIN_STMT if (status_44 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_45 = status_44; # DEBUG result => result_45 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT _46 = result_13; return _46; } FlexCAN_Ip_GetTDCValue_Privileged (uint8 u8Instance) { boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType result; uint8 value; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; long unsigned int _9; long unsigned int _10; unsigned char _11; uint8 _31; : # DEBUG BEGIN_STMT value_17 = 0; # DEBUG value => value_17 # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT _1 = u8Instance_19(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) u8Instance_19(D); pBase_22 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_22 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_22); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_24 = (boolean) _7; # DEBUG disabled => disabled_24 # DEBUG BEGIN_STMT if (disabled_24 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_26 = FlexCAN_Enable (pBase_22); # DEBUG result => result_26 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT if (result_13 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = FlexCAN_IsEnhCbtEnabled (pBase_22); if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 ={v} pBase_22->ETDC; value_29 = (uint8) _9; # DEBUG value => value_29 goto ; [INV] : # DEBUG BEGIN_STMT _10 ={v} pBase_22->FDCTRL; _11 = (unsigned char) _10; value_28 = _11 & 63; # DEBUG value => value_28 : # value_12 = PHI # DEBUG value => value_12 # DEBUG BEGIN_STMT if (disabled_24 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_Disable (pBase_22); : # DEBUG BEGIN_STMT _31 = value_12; return _31; } FlexCAN_Ip_GetTDCFail_Privileged (uint8 u8Instance) { boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType result; boolean value; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; boolean _32; : # DEBUG BEGIN_STMT value_18 = 0; # DEBUG value => value_18 # DEBUG BEGIN_STMT result_19 = 0; # DEBUG result => result_19 # DEBUG BEGIN_STMT _1 = u8Instance_20(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) u8Instance_20(D); pBase_23 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_23 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_23); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_25 = (boolean) _7; # DEBUG disabled => disabled_25 # DEBUG BEGIN_STMT if (disabled_25 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = FlexCAN_Enable (pBase_23); # DEBUG result => result_27 : # result_14 = PHI # DEBUG result => result_14 # DEBUG BEGIN_STMT if (result_14 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = FlexCAN_IsEnhCbtEnabled (pBase_23); if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 ={v} pBase_23->ETDC; _10 = _9 & 32768; value_30 = _10 == 32768; # DEBUG value => value_30 goto ; [INV] : # DEBUG BEGIN_STMT _11 ={v} pBase_23->FDCTRL; _12 = _11 & 16384; value_29 = _12 == 16384; # DEBUG value => value_29 : # value_13 = PHI # DEBUG value => value_13 # DEBUG BEGIN_STMT if (disabled_25 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_Disable (pBase_23); : # DEBUG BEGIN_STMT _32 = value_13; return _32; } FlexCAN_Ip_ClearTDCFail_Privileged (uint8 u8Instance) { boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; : # DEBUG BEGIN_STMT result_17 = 0; # DEBUG result => result_17 # DEBUG BEGIN_STMT _1 = u8Instance_18(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) u8Instance_18(D); pBase_21 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_21 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_21); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_23 = (boolean) _7; # DEBUG disabled => disabled_23 # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_25 = FlexCAN_Enable (pBase_21); # DEBUG result => result_25 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT if (result_13 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = FlexCAN_IsEnhCbtEnabled (pBase_21); if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 ={v} pBase_21->ETDC; _10 = _9 | 32768; pBase_21->ETDC ={v} _10; goto ; [INV] : # DEBUG BEGIN_STMT _11 ={v} pBase_21->FDCTRL; _12 = _11 | 16384; pBase_21->FDCTRL ={v} _12; : # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_Disable (pBase_21); : return; } FlexCAN_Ip_GetBitrate (uint8 instance, struct Flexcan_Ip_TimeSegmentType * bitrate) { boolean enhCbt; const struct FLEXCAN_Type * pBase; _Bool _1; _Bool _2; int _3; _Bool _4; boolean _19; : # DEBUG BEGIN_STMT _1 = instance_6(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = bitrate_9(D) != 0B; DevAssert (_2); # DEBUG BEGIN_STMT _3 = (int) instance_6(D); pBase_11 = g_Flexcan_Ip_aBase[_3]; # DEBUG pBase => pBase_11 # DEBUG BEGIN_STMT enhCbt_12 = 0; # DEBUG enhCbt => enhCbt_12 # DEBUG BEGIN_STMT enhCbt_14 = FlexCAN_IsEnhCbtEnabled (pBase_11); # DEBUG enhCbt => enhCbt_14 # DEBUG BEGIN_STMT if (enhCbt_14 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_GetEnhancedNominalTimeSegments (pBase_11, bitrate_9(D)); goto ; [INV] : # DEBUG BEGIN_STMT _4 = FlexCAN_IsExCbtEnabled (pBase_11); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_GetExtendedTimeSegments (pBase_11, bitrate_9(D)); goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_GetTimeSegments (pBase_11, bitrate_9(D)); : # DEBUG BEGIN_STMT _19 = enhCbt_14; return _19; } FlexCAN_Ip_SetBitrate_Privileged (uint8 instance, const struct Flexcan_Ip_TimeSegmentType * bitrate, boolean enhExt) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; _Bool _2; int _3; _Bool _4; int _5; _Bool _6; _Bool _7; int _8; _Bool _9; _Bool _10; Flexcan_Ip_StatusType _44; : # DEBUG BEGIN_STMT _1 = instance_18(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = bitrate_21(D) != 0B; DevAssert (_2); # DEBUG BEGIN_STMT result_23 = 0; # DEBUG result => result_23 # DEBUG BEGIN_STMT status_24 = 0; # DEBUG status => status_24 # DEBUG BEGIN_STMT _3 = (int) instance_18(D); pBase_25 = g_Flexcan_Ip_aBase[_3]; # DEBUG pBase => pBase_25 # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnabled (pBase_25); _5 = (int) _4; _6 = _5 != 0; _7 = ~_6; _8 = (int) _7; disabled_27 = (boolean) _8; # DEBUG disabled => disabled_27 # DEBUG BEGIN_STMT if (disabled_27 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_29 = FlexCAN_Enable (pBase_25); # DEBUG result => result_29 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT freeze_31 = FlexCAN_IsFreezeMode (pBase_25); # DEBUG freeze => freeze_31 # DEBUG BEGIN_STMT _9 = ~freeze_31; if (_9 != 0) goto ; [INV] else goto ; [INV] : if (result_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_32 = 1; # DEBUG result => result_32 : # result_12 = PHI # DEBUG result => result_12 # DEBUG BEGIN_STMT if (result_12 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_14 (); # DEBUG BEGIN_STMT FlexCAN_EnhCbtEnable (pBase_25, enhExt_34(D)); # DEBUG BEGIN_STMT if (enhExt_34(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedNominalTimeSegments (pBase_25, bitrate_21(D)); goto ; [INV] : # DEBUG BEGIN_STMT _10 = FlexCAN_IsExCbtEnabled (pBase_25); if (_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetExtendedTimeSegments (pBase_25, bitrate_21(D)); goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetTimeSegments (pBase_25, bitrate_21(D)); : # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_14 (); : # DEBUG BEGIN_STMT if (disabled_27 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_42 = FlexCAN_Disable (pBase_25); # DEBUG status => status_42 # DEBUG BEGIN_STMT if (status_42 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_43 = status_42; # DEBUG result => result_43 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT _44 = result_13; return _44; } FlexCAN_Ip_SetRxMaskType_Privileged (uint8 instance, Flexcan_Ip_RxMaskType type) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _33; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_22 = (boolean) _7; # DEBUG disabled => disabled_22 # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_24 = FlexCAN_Enable (pBase_20); # DEBUG result => result_24 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_26 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_26 # DEBUG BEGIN_STMT _8 = ~freeze_26; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = 1; # DEBUG result => result_27 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetRxMaskType (pBase_20, type_28(D)); : # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_31 = FlexCAN_Disable (pBase_20); # DEBUG status => status_31 # DEBUG BEGIN_STMT if (status_31 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_32 = status_31; # DEBUG result => result_32 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _33 = result_11; return _33; } FlexCAN_Ip_SetStopMode_Privileged (uint8 instance) { Flexcan_Ip_StatusType status; struct FLEXCAN_Type * pBase; _Bool _1; int _2; Flexcan_Ip_StatusType _13; : # DEBUG BEGIN_STMT _1 = instance_5(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) instance_5(D); pBase_8 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_8 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT status_10 = FlexCAN_EnterFreezeMode (pBase_8); # DEBUG status => status_10 # DEBUG BEGIN_STMT if (status_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_12 = FlexCAN_Disable (pBase_8); # DEBUG status => status_12 : # status_3 = PHI # DEBUG status => status_3 # DEBUG BEGIN_STMT _13 = status_3; return _13; } FlexCAN_Ip_SetStartMode_Privileged (uint8 instance) { struct FLEXCAN_Type * pBase; _Bool _1; int _2; long unsigned int _3; long unsigned int _4; Flexcan_Ip_StatusType _11; : # DEBUG BEGIN_STMT _1 = instance_5(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) instance_5(D); pBase_8 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_8 # DEBUG BEGIN_STMT _3 ={v} pBase_8->MCR; _4 = _3 & 2147483647; pBase_8->MCR ={v} _4; # DEBUG BEGIN_STMT _11 = FlexCAN_ExitFreezeMode (pBase_8); return _11; } FlexCAN_Ip_GetStartMode_Privileged (uint8 instance) { const struct FLEXCAN_Type * base; int _1; long unsigned int _2; long unsigned int _3; boolean _7; : # DEBUG BEGIN_STMT _1 = (int) instance_4(D); base_6 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_6 # DEBUG BEGIN_STMT _2 ={v} base_6->MCR; _3 = _2 & 17825792; _7 = _3 == 0; return _7; } FlexCAN_Ip_GetStopMode_Privileged (uint8 instance) { const struct FLEXCAN_Type * base; int _1; long unsigned int _2; long unsigned int _3; boolean _7; : # DEBUG BEGIN_STMT _1 = (int) instance_4(D); base_6 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_6 # DEBUG BEGIN_STMT _2 ={v} base_6->MCR; _3 = _2 & 1048576; _7 = _3 == 1048576; return _7; } FlexCAN_Ip_MainFunctionWrite (uint8 instance, uint8 mb_idx) { struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; _Bool _3; long unsigned int _4; unsigned char _5; long unsigned int _6; int _7; long unsigned int _8; long unsigned int _9; int _10; : # DEBUG BEGIN_STMT _1 = (int) instance_12(D); base_14 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_14 # DEBUG BEGIN_STMT _2 = (int) instance_12(D); state_15 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_15 # DEBUG BEGIN_STMT _3 = instance_12(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = (long unsigned int) mb_idx_17(D); _5 = FlexCAN_GetBuffStatusFlag (base_14, _4); if (_5 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = (long unsigned int) mb_idx_17(D); _7 = (int) mb_idx_17(D); _8 = FlexCAN_GetMsgBuffTimestamp (base_14, _6); state_15->mbs[_7].time_stamp = _8; # DEBUG BEGIN_STMT FlexCAN_UnlockRxMsgBuff (base_14); # DEBUG BEGIN_STMT _9 = (long unsigned int) mb_idx_17(D); FlexCAN_ClearMsgBuffIntStatusFlag (base_14, _9); # DEBUG BEGIN_STMT _10 = (int) mb_idx_17(D); state_15->mbs[_10].state ={v} 0; : return; } FlexCAN_Ip_MainFunctionBusOff_Privileged (uint8 instance) { uint32 u32ErrStatus; const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; Flexcan_Ip_StatusType eRetVal; int _1; int _2; _Bool _3; long unsigned int _4; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _5; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _6; Flexcan_Ip_StatusType _21; : # DEBUG BEGIN_STMT eRetVal_10 = 1; # DEBUG eRetVal => eRetVal_10 # DEBUG BEGIN_STMT _1 = (int) instance_11(D); base_13 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_13 # DEBUG BEGIN_STMT _2 = (int) instance_11(D); state_14 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_14 # DEBUG BEGIN_STMT u32ErrStatus_15 = 0; # DEBUG u32ErrStatus => u32ErrStatus_15 # DEBUG BEGIN_STMT _3 = instance_11(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT u32ErrStatus_17 ={v} base_13->ESR1; # DEBUG u32ErrStatus => u32ErrStatus_17 # DEBUG BEGIN_STMT _4 = u32ErrStatus_17 & 4; if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = state_14->error_callback; if (_5 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = state_14->error_callback; _6 (instance_11(D), 11, u32ErrStatus_17, state_14); : # DEBUG BEGIN_STMT base_13->ESR1 ={v} 4; # DEBUG BEGIN_STMT eRetVal_20 = 0; # DEBUG eRetVal => eRetVal_20 : # eRetVal_7 = PHI # DEBUG eRetVal => eRetVal_7 # DEBUG BEGIN_STMT _21 = eRetVal_7; return _21; } FlexCAN_Ip_MainFunctionRead (uint8 instance, uint8 mb_idx) { const struct Flexcan_Ip_StateType * state; const struct FLEXCAN_Type * base; int _1; int _2; _Bool _3; unsigned char _4; _Bool _5; _Bool _6; _Bool _7; unsigned char _8; _Bool _9; unsigned char _10; long unsigned int _11; unsigned char _12; int _13; _14; long unsigned int _15; : # DEBUG BEGIN_STMT _1 = (int) instance_17(D); base_19 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_19 # DEBUG BEGIN_STMT _2 = (int) instance_17(D); state_20 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_20 # DEBUG BEGIN_STMT _3 = instance_17(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = mb_idx_22(D) + 160; _5 = _4 > 158; DevAssert (_5); # DEBUG BEGIN_STMT if (mb_idx_22(D) == 255) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = FlexCAN_IsEnhancedRxFifoAvailable (base_19); if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = FlexCAN_IsEnhancedRxFifoEnabled (base_19); if (_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = FlexCAN_GetEnhancedRxFIFOStatusFlag (base_19, 28); if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerEnhancedRxFIFO (instance_17(D), 28); goto ; [INV] : # DEBUG BEGIN_STMT _9 = state_20->bIsLegacyFifoEn; if (_9 != 0) goto ; [INV] else goto ; [INV] : if (mb_idx_22(D) <= 7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (mb_idx_22(D) == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _10 = FlexCAN_GetBuffStatusFlag (base_19, 5); if (_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerRxFIFO (instance_17(D), 5); goto ; [INV] : # DEBUG BEGIN_STMT _11 = (long unsigned int) mb_idx_22(D); _12 = FlexCAN_GetBuffStatusFlag (base_19, _11); if (_12 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = (int) mb_idx_22(D); _14 ={v} state_20->mbs[_13].state; if (_14 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _15 = (long unsigned int) mb_idx_22(D); FlexCAN_IRQHandlerRxMB (instance_17(D), _15); : return; } FlexCAN_Ip_Deinit_Privileged (uint8 instance) { Flexcan_Ip_StatusType result; struct FLEXCAN_Type * base; int _1; _Bool _2; int _3; Flexcan_Ip_StatusType _15; : # DEBUG BEGIN_STMT _1 = (int) instance_5(D); base_7 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_7 # DEBUG BEGIN_STMT result_8 = 1; # DEBUG result => result_8 # DEBUG BEGIN_STMT _2 = instance_5(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT result_11 = FlexCAN_EnterFreezeMode (base_7); # DEBUG result => result_11 # DEBUG BEGIN_STMT if (result_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetRegDefaultVal (base_7); # DEBUG BEGIN_STMT FlexCAN_Disable (base_7); # DEBUG BEGIN_STMT _3 = (int) instance_5(D); g_flexcan_Ip_StatePtr[_3] = 0B; : # DEBUG BEGIN_STMT _15 = result_11; return _15; } FlexCAN_Ip_SetRxFifoGlobalMask_Privileged (uint8 instance, uint32 mask) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _33; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_22 = (boolean) _7; # DEBUG disabled => disabled_22 # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_24 = FlexCAN_Enable (pBase_20); # DEBUG result => result_24 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_26 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_26 # DEBUG BEGIN_STMT _8 = ~freeze_26; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = 1; # DEBUG result => result_27 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetRxFifoGlobalMask (pBase_20, mask_28(D)); : # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_31 = FlexCAN_Disable (pBase_20); # DEBUG status => status_31 # DEBUG BEGIN_STMT if (status_31 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_32 = status_31; # DEBUG result => result_32 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _33 = result_11; return _33; } FlexCAN_Ip_SetRxIndividualMask_Privileged (uint8 instance, uint8 mb_idx, uint32 mask) { boolean disabled; boolean freeze; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; int _1; _Bool _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; _Bool _6; int _7; _Bool _8; _Bool _9; int _10; _Bool _11; long unsigned int _12; Flexcan_Ip_StatusType _40; : # DEBUG BEGIN_STMT result_19 = 0; # DEBUG result => result_19 # DEBUG BEGIN_STMT status_20 = 0; # DEBUG status => status_20 # DEBUG BEGIN_STMT _1 = (int) instance_21(D); pBase_23 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_23 # DEBUG BEGIN_STMT freeze_24 = 0; # DEBUG freeze => freeze_24 # DEBUG BEGIN_STMT _2 = instance_21(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 = (long unsigned int) mb_idx_26(D); _4 ={v} pBase_23->MCR; _5 = _4 & 127; if (_3 > _5) goto ; [INV] else goto ; [INV] : if (mb_idx_26(D) > 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_39 = 4; # DEBUG result => result_39 goto ; [INV] : # DEBUG BEGIN_STMT _6 = FlexCAN_IsEnabled (pBase_23); _7 = (int) _6; _8 = _7 != 0; _9 = ~_8; _10 = (int) _9; disabled_28 = (boolean) _10; # DEBUG disabled => disabled_28 # DEBUG BEGIN_STMT if (disabled_28 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_30 = FlexCAN_Enable (pBase_23); # DEBUG result => result_30 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT freeze_32 = FlexCAN_IsFreezeMode (pBase_23); # DEBUG freeze => freeze_32 # DEBUG BEGIN_STMT _11 = ~freeze_32; if (_11 != 0) goto ; [INV] else goto ; [INV] : if (result_13 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_33 = 1; # DEBUG result => result_33 : # result_14 = PHI # DEBUG result => result_14 # DEBUG BEGIN_STMT if (result_14 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _12 = (long unsigned int) mb_idx_26(D); FlexCAN_SetRxIndividualMask (pBase_23, _12, mask_34(D)); : # DEBUG BEGIN_STMT if (disabled_28 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_37 = FlexCAN_Disable (pBase_23); # DEBUG status => status_37 # DEBUG BEGIN_STMT if (status_37 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_38 = status_37; # DEBUG result => result_38 : # result_15 = PHI # DEBUG result => result_15 # DEBUG BEGIN_STMT _40 = result_15; return _40; } FlexCAN_Ip_ExitFreezeMode_Privileged (uint8 instance) { struct FLEXCAN_Type * base; int _1; Flexcan_Ip_StatusType _6; : # DEBUG BEGIN_STMT _1 = (int) instance_2(D); base_4 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_4 # DEBUG BEGIN_STMT _6 = FlexCAN_ExitFreezeMode (base_4); return _6; } FlexCAN_Ip_EnterFreezeMode_Privileged (uint8 instance) { struct FLEXCAN_Type * base; int _1; Flexcan_Ip_StatusType _6; : # DEBUG BEGIN_STMT _1 = (int) instance_2(D); base_4 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_4 # DEBUG BEGIN_STMT _6 = FlexCAN_EnterFreezeMode (base_4); return _6; } FlexCAN_Ip_SetRxMbGlobalMask_Privileged (uint8 instance, uint32 mask) { boolean disabled; boolean freeze; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; int _1; _Bool _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _34; : # DEBUG BEGIN_STMT result_15 = 0; # DEBUG result => result_15 # DEBUG BEGIN_STMT status_16 = 0; # DEBUG status => status_16 # DEBUG BEGIN_STMT _1 = (int) instance_17(D); pBase_19 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_19 # DEBUG BEGIN_STMT freeze_20 = 0; # DEBUG freeze => freeze_20 # DEBUG BEGIN_STMT _2 = instance_17(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_19); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_23 = (boolean) _7; # DEBUG disabled => disabled_23 # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_25 = FlexCAN_Enable (pBase_19); # DEBUG result => result_25 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_27 = FlexCAN_IsFreezeMode (pBase_19); # DEBUG freeze => freeze_27 # DEBUG BEGIN_STMT _8 = ~freeze_27; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_28 = 1; # DEBUG result => result_28 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetRxMsgBuffGlobalMask (pBase_19, mask_29(D)); : # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_32 = FlexCAN_Disable (pBase_19); # DEBUG status => status_32 # DEBUG BEGIN_STMT if (status_32 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_33 = status_32; # DEBUG result => result_33 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _34 = result_11; return _34; } FlexCAN_Ip_SendBlocking (uint8 instance, uint8 mb_idx, const struct Flexcan_Ip_DataInfoType * tx_info, uint32 msg_id, const uint8 * mb_data, uint32 timeout_ms) { volatile uint32 * flexcan_mb; uint32 flexcan_mb_config; uint32 uS2Ticks; uint32 mS2Ticks; uint32 timeElapsed; uint32 timeStart; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; Flexcan_Ip_StatusType result; int _1; int _2; long unsigned int _3; long unsigned int _4; _Bool _5; _Bool _6; long unsigned int _7; unsigned char _8; int _9; _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; unsigned char _15; long unsigned int _16; long unsigned int _17; long unsigned int _18; long unsigned int _19; long unsigned int _20; int _21; long unsigned int _58; long unsigned int _75; Flexcan_Ip_StatusType _83; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = (int) instance_35(D); base_37 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_37 # DEBUG BEGIN_STMT _2 = (int) instance_35(D); state_38 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_38 # DEBUG BEGIN_STMT _3 = OsIf_GetCounter (0); timeStart = _3; # DEBUG BEGIN_STMT timeElapsed_41 = 0; # DEBUG timeElapsed => timeElapsed_41 # DEBUG BEGIN_STMT _4 = timeout_ms_42(D) * 1000; mS2Ticks_44 = OsIf_MicrosToTicks (_4, 0); # DEBUG mS2Ticks => mS2Ticks_44 # DEBUG BEGIN_STMT uS2Ticks_45 = 0; # DEBUG uS2Ticks => uS2Ticks_45 # DEBUG BEGIN_STMT flexcan_mb_config_46 = 0; # DEBUG flexcan_mb_config => flexcan_mb_config_46 # DEBUG BEGIN_STMT flexcan_mb_47 = 0B; # DEBUG flexcan_mb => flexcan_mb_47 # DEBUG BEGIN_STMT _5 = instance_35(D) <= 5; DevAssert (_5); # DEBUG BEGIN_STMT _6 = tx_info_49(D) != 0B; DevAssert (_6); # DEBUG BEGIN_STMT result_55 = FlexCAN_StartSendData (instance_35(D), mb_idx_51(D), tx_info_49(D), msg_id_52(D), mb_data_53(D)); # DEBUG result => result_55 # DEBUG BEGIN_STMT if (result_55 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _58 = OsIf_GetElapsed (&timeStart, 0); timeElapsed_59 = _58 + timeElapsed_27; # DEBUG timeElapsed => timeElapsed_59 # DEBUG BEGIN_STMT if (timeElapsed_59 >= mS2Ticks_44) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_60 = 3; # DEBUG result => result_60 # DEBUG BEGIN_STMT goto ; [INV] : # timeElapsed_27 = PHI # DEBUG timeElapsed => timeElapsed_27 # DEBUG BEGIN_STMT _7 = (long unsigned int) mb_idx_51(D); _8 = FlexCAN_GetBuffStatusFlag (base_37, _7); if (_8 != 1) goto ; [INV] else goto ; [INV] : # result_22 = PHI # DEBUG result => result_22 # DEBUG BEGIN_STMT if (result_22 == 3) goto ; [INV] else goto ; [INV] : _9 = (int) mb_idx_51(D); _10 ={v} state_38->mbs[_9].state; if (_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 = (long unsigned int) mb_idx_51(D); FlexCAN_ClearMsgBuffIntStatusFlag (base_37, _11); # DEBUG BEGIN_STMT _12 = (long unsigned int) mb_idx_51(D); flexcan_mb_63 = FlexCAN_GetMsgBuffRegion (base_37, _12); # DEBUG flexcan_mb => flexcan_mb_63 # DEBUG BEGIN_STMT flexcan_mb_config_64 ={v} *flexcan_mb_63; # DEBUG flexcan_mb_config => flexcan_mb_config_64 # DEBUG BEGIN_STMT flexcan_mb_config_65 = flexcan_mb_config_64 & 4043309055; # DEBUG flexcan_mb_config => flexcan_mb_config_65 # DEBUG BEGIN_STMT flexcan_mb_config_66 = flexcan_mb_config_65 | 150994944; # DEBUG flexcan_mb_config => flexcan_mb_config_66 # DEBUG BEGIN_STMT *flexcan_mb_63 ={v} flexcan_mb_config_66; # DEBUG BEGIN_STMT uS2Ticks_69 = OsIf_MicrosToTicks (100, 0); # DEBUG uS2Ticks => uS2Ticks_69 # DEBUG BEGIN_STMT _13 = OsIf_GetCounter (0); timeStart = _13; # DEBUG BEGIN_STMT timeElapsed_72 = 0; # DEBUG timeElapsed => timeElapsed_72 # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT _75 = OsIf_GetElapsed (&timeStart, 0); timeElapsed_76 = _75 + timeElapsed_28; # DEBUG timeElapsed => timeElapsed_76 # DEBUG BEGIN_STMT if (timeElapsed_76 >= uS2Ticks_69) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_77 = 3; # DEBUG result => result_77 # DEBUG BEGIN_STMT goto ; [INV] : # timeElapsed_28 = PHI # DEBUG timeElapsed => timeElapsed_28 # DEBUG BEGIN_STMT _14 = (long unsigned int) mb_idx_51(D); _15 = FlexCAN_GetBuffStatusFlag (base_37, _14); if (_15 == 0) goto ; [INV] else goto ; [INV] : # result_23 = PHI # DEBUG result => result_23 # DEBUG BEGIN_STMT flexcan_mb_config_78 ={v} *flexcan_mb_63; # DEBUG flexcan_mb_config => flexcan_mb_config_78 # DEBUG BEGIN_STMT _16 = flexcan_mb_config_78 >> 24; _17 = _16 & 15; if (_17 == 8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_79 = 0; # DEBUG result => result_79 : # result_24 = PHI # DEBUG result => result_24 # DEBUG BEGIN_STMT _18 = flexcan_mb_config_78 >> 24; _19 = _18 & 15; if (_19 == 9) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_80 = 3; # DEBUG result => result_80 : # result_25 = PHI # DEBUG result => result_25 # DEBUG BEGIN_STMT _20 = (long unsigned int) mb_idx_51(D); FlexCAN_ClearMsgBuffIntStatusFlag (base_37, _20); # DEBUG BEGIN_STMT _21 = (int) mb_idx_51(D); state_38->mbs[_21].state ={v} 0; : # result_26 = PHI # DEBUG result => result_26 # DEBUG BEGIN_STMT _83 = result_26; timeStart ={v} {CLOBBER}; return _83; } FlexCAN_Busoff_Error_IRQHandler (uint8 instance) { boolean isSpuriousInt; uint32 u32ErrStatus; const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * pBase; int _1; int _2; _Bool _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _7; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _8; long unsigned int _9; long unsigned int _10; signed int _11; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _12; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _13; long unsigned int _14; long unsigned int _15; long unsigned int _16; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _17; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _18; long unsigned int _19; long unsigned int _20; long unsigned int _21; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _22; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _23; long unsigned int _24; long unsigned int _25; long unsigned int _26; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _27; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _28; : # DEBUG BEGIN_STMT _1 = (int) instance_53(D); pBase_55 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_55 # DEBUG BEGIN_STMT _2 = (int) instance_53(D); state_56 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_56 # DEBUG BEGIN_STMT u32ErrStatus_57 = 0; # DEBUG u32ErrStatus => u32ErrStatus_57 # DEBUG BEGIN_STMT isSpuriousInt_58 = 1; # DEBUG isSpuriousInt => isSpuriousInt_58 # DEBUG BEGIN_STMT _3 = instance_53(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT if (state_56 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT u32ErrStatus_60 ={v} pBase_55->ESR1; # DEBUG u32ErrStatus => u32ErrStatus_60 # DEBUG BEGIN_STMT _4 = u32ErrStatus_60 & 2; if (_4 != 0) goto ; [INV] else goto ; [INV] : _5 ={v} pBase_55->CTRL1; _6 = _5 & 16384; if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_55->ESR1 ={v} 2; # DEBUG BEGIN_STMT _7 = state_56->error_callback; if (_7 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = state_56->error_callback; _8 (instance_53(D), 9, u32ErrStatus_60, state_56); # DEBUG BEGIN_STMT u32ErrStatus_63 ={v} pBase_55->ESR1; # DEBUG u32ErrStatus => u32ErrStatus_63 : # u32ErrStatus_29 = PHI # DEBUG u32ErrStatus => u32ErrStatus_29 # DEBUG BEGIN_STMT isSpuriousInt_64 = 0; # DEBUG isSpuriousInt => isSpuriousInt_64 : # u32ErrStatus_30 = PHI # isSpuriousInt_37 = PHI # DEBUG isSpuriousInt => isSpuriousInt_37 # DEBUG u32ErrStatus => u32ErrStatus_30 # DEBUG BEGIN_STMT _9 = u32ErrStatus_30 & 1048576; if (_9 != 0) goto ; [INV] else goto ; [INV] : _10 ={v} pBase_55->CTRL2; _11 = (signed int) _10; if (_11 < 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_55->ESR1 ={v} 1048576; # DEBUG BEGIN_STMT _12 = state_56->error_callback; if (_12 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = state_56->error_callback; _13 (instance_53(D), 10, u32ErrStatus_30, state_56); # DEBUG BEGIN_STMT u32ErrStatus_67 ={v} pBase_55->ESR1; # DEBUG u32ErrStatus => u32ErrStatus_67 : # u32ErrStatus_31 = PHI # DEBUG u32ErrStatus => u32ErrStatus_31 # DEBUG BEGIN_STMT isSpuriousInt_68 = 0; # DEBUG isSpuriousInt => isSpuriousInt_68 : # u32ErrStatus_32 = PHI # isSpuriousInt_38 = PHI # DEBUG isSpuriousInt => isSpuriousInt_38 # DEBUG u32ErrStatus => u32ErrStatus_32 # DEBUG BEGIN_STMT _14 = u32ErrStatus_32 & 131072; if (_14 != 0) goto ; [INV] else goto ; [INV] : _15 ={v} pBase_55->CTRL1; _16 = _15 & 2048; if (_16 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_55->ESR1 ={v} 131072; # DEBUG BEGIN_STMT _17 = state_56->error_callback; if (_17 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _18 = state_56->error_callback; _18 (instance_53(D), 13, u32ErrStatus_32, state_56); # DEBUG BEGIN_STMT u32ErrStatus_71 ={v} pBase_55->ESR1; # DEBUG u32ErrStatus => u32ErrStatus_71 : # u32ErrStatus_33 = PHI # DEBUG u32ErrStatus => u32ErrStatus_33 # DEBUG BEGIN_STMT isSpuriousInt_72 = 0; # DEBUG isSpuriousInt => isSpuriousInt_72 : # u32ErrStatus_34 = PHI # isSpuriousInt_39 = PHI # DEBUG isSpuriousInt => isSpuriousInt_39 # DEBUG u32ErrStatus => u32ErrStatus_34 # DEBUG BEGIN_STMT _19 = u32ErrStatus_34 & 65536; if (_19 != 0) goto ; [INV] else goto ; [INV] : _20 ={v} pBase_55->CTRL1; _21 = _20 & 1024; if (_21 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_55->ESR1 ={v} 65536; # DEBUG BEGIN_STMT _22 = state_56->error_callback; if (_22 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _23 = state_56->error_callback; _23 (instance_53(D), 12, u32ErrStatus_34, state_56); # DEBUG BEGIN_STMT u32ErrStatus_75 ={v} pBase_55->ESR1; # DEBUG u32ErrStatus => u32ErrStatus_75 : # u32ErrStatus_35 = PHI # DEBUG u32ErrStatus => u32ErrStatus_35 # DEBUG BEGIN_STMT isSpuriousInt_76 = 0; # DEBUG isSpuriousInt => isSpuriousInt_76 : # u32ErrStatus_36 = PHI # isSpuriousInt_40 = PHI # DEBUG isSpuriousInt => isSpuriousInt_40 # DEBUG u32ErrStatus => u32ErrStatus_36 # DEBUG BEGIN_STMT _24 = u32ErrStatus_36 & 4; if (_24 != 0) goto ; [INV] else goto ; [INV] : _25 ={v} pBase_55->CTRL1; _26 = _25 & 32768; if (_26 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_55->ESR1 ={v} 4; # DEBUG BEGIN_STMT _27 = state_56->error_callback; if (_27 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _28 = state_56->error_callback; _28 (instance_53(D), 11, u32ErrStatus_36, state_56); : # DEBUG BEGIN_STMT isSpuriousInt_79 = 0; # DEBUG isSpuriousInt => isSpuriousInt_79 : # isSpuriousInt_41 = PHI # DEBUG isSpuriousInt => isSpuriousInt_41 # DEBUG BEGIN_STMT if (isSpuriousInt_41 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pBase_55->ESR1 ={v} 3866630; : return; } FlexCAN_Ip_GetControllerRxErrorCounter (uint8 instance) { const struct FLEXCAN_Type * base; int _1; _Bool _2; long unsigned int _3; long unsigned int _4; uint8 _9; : # DEBUG BEGIN_STMT _1 = (int) instance_5(D); base_7 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_7 # DEBUG BEGIN_STMT _2 = instance_5(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 ={v} base_7->ECR; _4 = _3 >> 8; _9 = (uint8) _4; return _9; } FlexCAN_Ip_GetControllerTxErrorCounter (uint8 instance) { const struct FLEXCAN_Type * base; int _1; _Bool _2; long unsigned int _3; uint8 _8; : # DEBUG BEGIN_STMT _1 = (int) instance_4(D); base_6 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_6 # DEBUG BEGIN_STMT _2 = instance_4(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 ={v} base_6->ECR; _8 = (uint8) _3; return _8; } FlexCAN_Ip_GetErrorStatus (uint8 instance) { const struct FLEXCAN_Type * base; int _1; _Bool _2; uint32 _7; : # DEBUG BEGIN_STMT _1 = (int) instance_3(D); base_5 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_5 # DEBUG BEGIN_STMT _2 = instance_3(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _7 ={v} base_5->ESR1; return _7; } FlexCAN_Ip_ClearErrorStatus (uint8 instance, uint32 error) { struct FLEXCAN_Type * base; int _1; _Bool _2; : # DEBUG BEGIN_STMT _1 = (int) instance_3(D); base_5 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_5 # DEBUG BEGIN_STMT _2 = instance_3(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT base_5->ESR1 ={v} error_7(D); return; } FlexCAN_IRQHandler (uint8 instance, uint32 startMbIdx, uint32 endMbIdx, boolean bEnhancedFifoExisted) { uint32 mb_idx; boolean bIsSpuriousInt; const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; uint32 flag_reg; uint32 u32MbHandle; int _1; int _2; _Bool _3; _Bool _4; unsigned char _5; unsigned char _6; _Bool _7; _8; _9; unsigned char _10; _11; _Bool _12; _13; : # DEBUG BEGIN_STMT u32MbHandle_27 = 0; # DEBUG u32MbHandle => u32MbHandle_27 # DEBUG BEGIN_STMT flag_reg_28 = 0; # DEBUG flag_reg => flag_reg_28 # DEBUG BEGIN_STMT _1 = (int) instance_29(D); base_31 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_31 # DEBUG BEGIN_STMT _2 = (int) instance_29(D); state_32 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_32 # DEBUG BEGIN_STMT bIsSpuriousInt_33 = 1; # DEBUG bIsSpuriousInt => bIsSpuriousInt_33 # DEBUG BEGIN_STMT mb_idx_35 = endMbIdx_34(D); # DEBUG mb_idx => mb_idx_35 # DEBUG BEGIN_STMT _3 = instance_29(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = endMbIdx_34(D) <= 95; DevAssert (_4); # DEBUG BEGIN_STMT if (state_32 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = FlexCAN_GetMsgBuffIntStatusFlag (base_31, mb_idx_35); flag_reg_48 = (uint32) _5; # DEBUG flag_reg => flag_reg_48 # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT mb_idx_49 = mb_idx_18 + 4294967295; # DEBUG mb_idx => mb_idx_49 # DEBUG BEGIN_STMT _6 = FlexCAN_GetMsgBuffIntStatusFlag (base_31, mb_idx_49); flag_reg_51 = (uint32) _6; # DEBUG flag_reg => flag_reg_51 : # flag_reg_15 = PHI # mb_idx_18 = PHI # DEBUG mb_idx => mb_idx_18 # DEBUG flag_reg => flag_reg_15 # DEBUG BEGIN_STMT if (flag_reg_15 == 0) goto ; [INV] else goto ; [INV] : if (mb_idx_18 > startMbIdx_38(D)) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (flag_reg_15 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT bIsSpuriousInt_52 = 0; # DEBUG bIsSpuriousInt => bIsSpuriousInt_52 # DEBUG BEGIN_STMT u32MbHandle_53 = mb_idx_18; # DEBUG u32MbHandle => u32MbHandle_53 # DEBUG BEGIN_STMT _7 = state_32->bIsLegacyFifoEn; if (_7 != 0) goto ; [INV] else goto ; [INV] : if (mb_idx_18 <= 7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerRxFIFO (instance_29(D), mb_idx_18); # DEBUG BEGIN_STMT u32MbHandle_55 = 0; # DEBUG u32MbHandle => u32MbHandle_55 goto ; [INV] : # DEBUG BEGIN_STMT _8 ={v} state_32->mbs[u32MbHandle_53].state; if (_8 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerRxMB (instance_29(D), mb_idx_18); : # u32MbHandle_14 = PHI # DEBUG u32MbHandle => u32MbHandle_14 # DEBUG BEGIN_STMT _9 ={v} state_32->mbs[u32MbHandle_14].state; if (_9 == 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerTxMB (instance_29(D), mb_idx_18); : # DEBUG BEGIN_STMT _10 = FlexCAN_GetMsgBuffIntStatusFlag (base_31, mb_idx_18); if (_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 ={v} state_32->mbs[u32MbHandle_14].state; if (_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_31, mb_idx_18); : # bIsSpuriousInt_16 = PHI # DEBUG bIsSpuriousInt => bIsSpuriousInt_16 # DEBUG BEGIN_STMT if (bEnhancedFifoExisted_40(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _12 = FlexCAN_IsEnhancedRxFifoEnabled (base_31); if (_12 != 0) goto ; [INV] else goto ; [INV] : _13 = state_32->transferType; if (_13 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT bIsSpuriousInt_62 = FlexCAN_ProcessIRQHandlerEnhancedRxFIFO (instance_29(D), bIsSpuriousInt_16); # DEBUG bIsSpuriousInt => bIsSpuriousInt_62 : # bIsSpuriousInt_17 = PHI # DEBUG bIsSpuriousInt => bIsSpuriousInt_17 # DEBUG BEGIN_STMT if (bIsSpuriousInt_17 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ProcessSpuriousInterruptMB (instance_29(D), startMbIdx_38(D), endMbIdx_34(D)); goto ; [INV] : # DEBUG BEGIN_STMT mb_idx_39 = startMbIdx_38(D); # DEBUG mb_idx => mb_idx_39 goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_31, mb_idx_19); # DEBUG BEGIN_STMT mb_idx_46 = mb_idx_19 + 1; # DEBUG mb_idx => mb_idx_46 : # mb_idx_19 = PHI # DEBUG mb_idx => mb_idx_19 # DEBUG BEGIN_STMT if (mb_idx_19 <= endMbIdx_34(D)) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (bEnhancedFifoExisted_40(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_31, 28); # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_31, 29); # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_31, 30); # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_31, 31); : return; } FlexCAN_CompleteRxMessageFifoData (uint8 instance) { struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; _Bool _3; _4; _Bool _5; _Bool _6; _Bool _7; : # DEBUG BEGIN_STMT _1 = (int) instance_9(D); base_11 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_11 # DEBUG BEGIN_STMT _2 = (int) instance_9(D); state_12 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_12 # DEBUG BEGIN_STMT _3 = instance_9(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = state_12->transferType; if (_4 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = state_12->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_11, instance_9(D), 5, 0, _5); # DEBUG BEGIN_STMT _6 = state_12->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_11, instance_9(D), 6, 0, _6); # DEBUG BEGIN_STMT _7 = state_12->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_11, instance_9(D), 7, 0, _7); : # DEBUG BEGIN_STMT state_12->mbs[0].pMBmessage = 0B; # DEBUG BEGIN_STMT state_12->mbs[0].state ={v} 0; return; } FlexCAN_Ip_GetTransferStatus (uint8 instance, uint8 mb_idx) { Flexcan_Ip_StatusType status; const struct Flexcan_Ip_StateType * state; int _1; _Bool _2; unsigned char _3; _Bool _4; int _5; _6; _7; Flexcan_Ip_StatusType _20; : # DEBUG BEGIN_STMT _1 = (int) instance_9(D); state_11 = g_flexcan_Ip_StatePtr[_1]; # DEBUG state => state_11 # DEBUG BEGIN_STMT status_12 = 1; # DEBUG status => status_12 # DEBUG BEGIN_STMT _2 = instance_9(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 = mb_idx_14(D) + 160; _4 = _3 > 158; DevAssert (_4); # DEBUG BEGIN_STMT if (mb_idx_14(D) <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = (int) mb_idx_14(D); _6 ={v} state_11->mbs[_5].state; if (_6 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 goto ; [INV] : # DEBUG BEGIN_STMT status_18 = 2; # DEBUG status => status_18 goto ; [INV] : # DEBUG BEGIN_STMT _7 ={v} state_11->enhancedFifoOutput.state; if (_7 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_17 = 0; # DEBUG status => status_17 goto ; [INV] : # DEBUG BEGIN_STMT status_16 = 2; # DEBUG status => status_16 : # status_8 = PHI # DEBUG status => status_8 # DEBUG BEGIN_STMT _20 = status_8; return _20; } FlexCAN_Ip_ConfigRemoteResponseMb (uint8 instance, uint8 mb_idx, const struct Flexcan_Ip_DataInfoType * tx_info, uint32 msg_id, const uint8 * mb_data) { const struct Flexcan_Ip_StateType * const state; struct FLEXCAN_Type * pBase; struct Flexcan_Ip_MsbuffCodeStatusType cs; Flexcan_Ip_StatusType result; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; long unsigned int _6; _Bool _7; long unsigned int _8; _9; long unsigned int _10; long unsigned int _11; _Bool _12; _Bool _13; _Bool _14; long unsigned int _15; _Bool _16; Flexcan_Ip_StatusType _41; : # DEBUG BEGIN_STMT result_20 = 0; # DEBUG result => result_20 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = (int) instance_21(D); pBase_23 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_23 # DEBUG BEGIN_STMT _2 = (int) instance_21(D); state_24 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_24 # DEBUG BEGIN_STMT _3 = instance_21(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = tx_info_26(D) != 0B; DevAssert (_4); # DEBUG BEGIN_STMT _5 = state_24->bIsLegacyFifoEn; _6 = state_24->u32MaxMbNum; _7 = FlexCAN_IsMbOutOfRange (pBase_23, mb_idx_28(D), _5, _6); if (_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_30 = 4; # DEBUG result => result_30 : # result_17 = PHI # DEBUG result => result_17 # DEBUG BEGIN_STMT if (result_17 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = tx_info_26(D)->data_length; cs.dataLen = _8; # DEBUG BEGIN_STMT _9 = tx_info_26(D)->msg_id_type; cs.msgIdType = _9; # DEBUG BEGIN_STMT cs.code = 10; # DEBUG BEGIN_STMT cs.fd_enable = 0; # DEBUG BEGIN_STMT _10 = (long unsigned int) mb_idx_28(D); FlexCAN_ClearMsgBuffIntStatusFlag (pBase_23, _10); # DEBUG BEGIN_STMT _11 = (long unsigned int) mb_idx_28(D); _12 = tx_info_26(D)->is_remote; FlexCAN_SetTxMsgBuff (pBase_23, _11, &cs, msg_id_36(D), mb_data_37(D), _12); # DEBUG BEGIN_STMT _13 = tx_info_26(D)->is_polling; _14 = ~_13; if (_14 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _15 = (long unsigned int) mb_idx_28(D); _16 = state_24->isIntActive; result_40 = FlexCAN_SetMsgBuffIntCmd (pBase_23, instance_21(D), _15, 1, _16); # DEBUG result => result_40 : # result_18 = PHI # DEBUG result => result_18 # DEBUG BEGIN_STMT _41 = result_18; cs ={v} {CLOBBER}; return _41; } FlexCAN_Ip_ConfigEnhancedRxFifo_Privileged (uint8 instance, const struct Flexcan_Ip_EnhancedIdTableType * id_filter_table) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; int _1; _Bool _2; int _3; _Bool _4; _Bool _5; int _6; _Bool _7; _Bool _8; _Bool _9; _Bool _10; Flexcan_Ip_StatusType _38; : # DEBUG BEGIN_STMT result_17 = 0; # DEBUG result => result_17 # DEBUG BEGIN_STMT status_18 = 0; # DEBUG status => status_18 # DEBUG BEGIN_STMT _1 = (int) instance_19(D); pBase_21 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_21 # DEBUG BEGIN_STMT _2 = FlexCAN_IsEnabled (pBase_21); _3 = (int) _2; _4 = _3 != 0; _5 = ~_4; _6 = (int) _5; disabled_23 = (boolean) _6; # DEBUG disabled => disabled_23 # DEBUG BEGIN_STMT _7 = instance_19(D) <= 5; DevAssert (_7); # DEBUG BEGIN_STMT _8 = FlexCAN_IsEnhancedRxFifoAvailable (pBase_21); DevAssert (_8); # DEBUG BEGIN_STMT _9 = id_filter_table_27(D) != 0B; DevAssert (_9); # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_30 = FlexCAN_Enable (pBase_21); # DEBUG result => result_30 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT freeze_32 = FlexCAN_IsFreezeMode (pBase_21); # DEBUG freeze => freeze_32 # DEBUG BEGIN_STMT _10 = ~freeze_32; if (_10 != 0) goto ; [INV] else goto ; [INV] : if (result_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_33 = 1; # DEBUG result => result_33 : # result_12 = PHI # DEBUG result => result_12 # DEBUG BEGIN_STMT if (result_12 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedRxFifoFilter (pBase_21, id_filter_table_27(D)); : # DEBUG BEGIN_STMT if (disabled_23 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_36 = FlexCAN_Disable (pBase_21); # DEBUG status => status_36 # DEBUG BEGIN_STMT if (status_36 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_37 = status_36; # DEBUG result => result_37 : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT _38 = result_13; return _38; } FlexCAN_Ip_ConfigRxFifo_Privileged (uint8 instance, Flexcan_Ip_RxFifoIdElementFormatType id_format, const struct Flexcan_Ip_IdTableType * id_filter_table) { boolean freeze; boolean disabled; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType status; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; int _4; _Bool _5; _Bool _6; int _7; _Bool _8; Flexcan_Ip_StatusType _34; : # DEBUG BEGIN_STMT _1 = instance_15(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT result_18 = 0; # DEBUG result => result_18 # DEBUG BEGIN_STMT status_19 = 0; # DEBUG status => status_19 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); pBase_20 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_20 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnabled (pBase_20); _4 = (int) _3; _5 = _4 != 0; _6 = ~_5; _7 = (int) _6; disabled_22 = (boolean) _7; # DEBUG disabled => disabled_22 # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_24 = FlexCAN_Enable (pBase_20); # DEBUG result => result_24 : # result_9 = PHI # DEBUG result => result_9 # DEBUG BEGIN_STMT freeze_26 = FlexCAN_IsFreezeMode (pBase_20); # DEBUG freeze => freeze_26 # DEBUG BEGIN_STMT _8 = ~freeze_26; if (_8 != 0) goto ; [INV] else goto ; [INV] : if (result_9 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = 1; # DEBUG result => result_27 : # result_10 = PHI # DEBUG result => result_10 # DEBUG BEGIN_STMT if (result_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetRxFifoFilter (pBase_20, id_format_28(D), id_filter_table_29(D)); : # DEBUG BEGIN_STMT if (disabled_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT status_32 = FlexCAN_Disable (pBase_20); # DEBUG status => status_32 # DEBUG BEGIN_STMT if (status_32 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_33 = status_32; # DEBUG result => result_33 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _34 = result_11; return _34; } FlexCAN_Ip_RxFifoBlocking (uint8 instance, struct Flexcan_Ip_MsgBuffType * data, uint32 timeout) { const struct FLEXCAN_Type * base; Flexcan_Ip_StatusType result; int _1; _Bool _2; _Bool _3; _Bool _4; Flexcan_Ip_StatusType _28; : # DEBUG BEGIN_STMT result_7 = 0; # DEBUG result => result_7 # DEBUG BEGIN_STMT _1 = (int) instance_8(D); base_10 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_10 # DEBUG BEGIN_STMT _2 = instance_8(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnhancedRxFifoAvailable (base_10); if (_3 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnhancedRxFifoEnabled (base_10); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_25 = FlexCAN_StartRxMessageEnhancedFifoData (instance_8(D), data_13(D)); # DEBUG result => result_25 # DEBUG BEGIN_STMT if (result_25 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = FlexCAN_ProccessEnhancedRxFifo (instance_8(D), timeout_16(D)); # DEBUG result => result_27 goto ; [INV] : # DEBUG BEGIN_STMT result_21 = FlexCAN_StartRxMessageFifoData (instance_8(D), data_13(D)); # DEBUG result => result_21 # DEBUG BEGIN_STMT if (result_21 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_23 = FlexCAN_ProccessLegacyRxFIFO (instance_8(D), timeout_16(D)); # DEBUG result => result_23 goto ; [INV] : # DEBUG BEGIN_STMT result_15 = FlexCAN_StartRxMessageFifoData (instance_8(D), data_13(D)); # DEBUG result => result_15 # DEBUG BEGIN_STMT if (result_15 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_18 = FlexCAN_ProccessLegacyRxFIFO (instance_8(D), timeout_16(D)); # DEBUG result => result_18 : # result_5 = PHI # DEBUG result => result_5 # DEBUG BEGIN_STMT _28 = result_5; return _28; } FlexCAN_Ip_RxFifo (uint8 instance, struct Flexcan_Ip_MsgBuffType * data) { const struct FLEXCAN_Type * base; Flexcan_Ip_StatusType result; _Bool _1; int _2; _Bool _3; _Bool _4; Flexcan_Ip_StatusType _21; : # DEBUG BEGIN_STMT result_7 = 0; # DEBUG result => result_7 # DEBUG BEGIN_STMT _1 = instance_8(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) instance_8(D); base_11 = g_Flexcan_Ip_aBase[_2]; # DEBUG base => base_11 # DEBUG BEGIN_STMT _3 = FlexCAN_IsEnhancedRxFifoAvailable (base_11); if (_3 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnhancedRxFifoEnabled (base_11); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_20 = FlexCAN_StartRxMessageEnhancedFifoData (instance_8(D), data_13(D)); # DEBUG result => result_20 goto ; [INV] : # DEBUG BEGIN_STMT result_18 = FlexCAN_StartRxMessageFifoData (instance_8(D), data_13(D)); # DEBUG result => result_18 goto ; [INV] : # DEBUG BEGIN_STMT result_15 = FlexCAN_StartRxMessageFifoData (instance_8(D), data_13(D)); # DEBUG result => result_15 : # result_5 = PHI # DEBUG result => result_5 # DEBUG BEGIN_STMT _21 = result_5; return _21; } FlexCAN_Ip_ReceiveBlocking (uint8 instance, uint8 mb_idx, struct Flexcan_Ip_MsgBuffType * data, boolean isPolling, uint32 u32TimeoutMs) { struct FLEXCAN_Type * base; struct Flexcan_Ip_StateType * state; uint32 mS2Ticks; uint32 timeElapsed; uint32 timeStart; Flexcan_Ip_StatusType result; long unsigned int _1; _Bool _2; int _3; int _4; _Bool _5; long unsigned int _6; _Bool _7; long unsigned int _8; long unsigned int _9; unsigned char _10; long unsigned int _11; int _12; _13; _Bool _14; long unsigned int _15; _Bool _16; int _17; _18; int _19; long unsigned int _52; Flexcan_Ip_StatusType _59; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT timeStart = 0; # DEBUG BEGIN_STMT timeElapsed_32 = 0; # DEBUG timeElapsed => timeElapsed_32 # DEBUG BEGIN_STMT _1 = u32TimeoutMs_33(D) * 1000; mS2Ticks_35 = OsIf_MicrosToTicks (_1, 0); # DEBUG mS2Ticks => mS2Ticks_35 # DEBUG BEGIN_STMT _2 = instance_36(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 = (int) instance_36(D); state_38 = g_flexcan_Ip_StatePtr[_3]; # DEBUG state => state_38 # DEBUG BEGIN_STMT _4 = (int) instance_36(D); base_39 = g_Flexcan_Ip_aBase[_4]; # DEBUG base => base_39 # DEBUG BEGIN_STMT result_44 = FlexCAN_StartRxMessageBufferData (instance_36(D), mb_idx_40(D), data_41(D), isPolling_42(D)); # DEBUG result => result_44 # DEBUG BEGIN_STMT if (result_44 == 0) goto ; [INV] else goto ; [INV] : _5 = ~isPolling_42(D); if (_5 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = (long unsigned int) mb_idx_40(D); _7 = state_38->isIntActive; result_46 = FlexCAN_SetMsgBuffIntCmd (base_39, instance_36(D), _6, 1, _7); # DEBUG result => result_46 : # result_20 = PHI # DEBUG result => result_20 # DEBUG BEGIN_STMT if (result_20 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = OsIf_GetCounter (0); timeStart = _8; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT if (isPolling_42(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = (long unsigned int) mb_idx_40(D); _10 = FlexCAN_GetBuffStatusFlag (base_39, _9); if (_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 = (long unsigned int) mb_idx_40(D); FlexCAN_IRQHandlerRxMB (instance_36(D), _11); : # DEBUG BEGIN_STMT _52 = OsIf_GetElapsed (&timeStart, 0); timeElapsed_53 = _52 + timeElapsed_23; # DEBUG timeElapsed => timeElapsed_53 # DEBUG BEGIN_STMT if (timeElapsed_53 >= mS2Ticks_35) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_54 = 3; # DEBUG result => result_54 # DEBUG BEGIN_STMT goto ; [INV] : # timeElapsed_23 = PHI # DEBUG timeElapsed => timeElapsed_23 # DEBUG BEGIN_STMT _12 = (int) mb_idx_40(D); _13 ={v} state_38->mbs[_12].state; if (_13 == 1) goto ; [INV] else goto ; [INV] : # result_21 = PHI # DEBUG result => result_21 # DEBUG BEGIN_STMT if (result_21 == 3) goto ; [INV] else goto ; [INV] : _14 = ~isPolling_42(D); if (_14 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _15 = (long unsigned int) mb_idx_40(D); _16 = state_38->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_39, instance_36(D), _15, 0, _16); : # DEBUG BEGIN_STMT if (result_21 != 4) goto ; [INV] else goto ; [INV] : if (result_21 != 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _17 = (int) mb_idx_40(D); _18 ={v} state_38->mbs[_17].state; if (_18 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_58 = 0; # DEBUG result => result_58 goto ; [INV] : # DEBUG BEGIN_STMT _19 = (int) mb_idx_40(D); state_38->mbs[_19].state ={v} 0; # DEBUG BEGIN_STMT result_57 = 3; # DEBUG result => result_57 : # result_22 = PHI # DEBUG result => result_22 # DEBUG BEGIN_STMT _59 = result_22; timeStart ={v} {CLOBBER}; return _59; } FlexCAN_Ip_Receive (uint8 instance, uint8 mb_idx, struct Flexcan_Ip_MsgBuffType * data, boolean isPolling) { const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; Flexcan_Ip_StatusType result; int _1; int _2; _Bool _3; _Bool _4; long unsigned int _5; _Bool _6; Flexcan_Ip_StatusType _21; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = (int) instance_9(D); base_11 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_11 # DEBUG BEGIN_STMT _2 = (int) instance_9(D); state_12 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_12 # DEBUG BEGIN_STMT _3 = instance_9(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT result_18 = FlexCAN_StartRxMessageBufferData (instance_9(D), mb_idx_14(D), data_15(D), isPolling_16(D)); # DEBUG result => result_18 # DEBUG BEGIN_STMT if (result_18 == 0) goto ; [INV] else goto ; [INV] : _4 = ~isPolling_16(D); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = (long unsigned int) mb_idx_14(D); _6 = state_12->isIntActive; result_20 = FlexCAN_SetMsgBuffIntCmd (base_11, instance_9(D), _5, 1, _6); # DEBUG result => result_20 : # result_7 = PHI # DEBUG result => result_7 # DEBUG BEGIN_STMT _21 = result_7; return _21; } FlexCAN_Ip_ConfigRxMb (uint8 instance, uint8 mb_idx, const struct Flexcan_Ip_DataInfoType * rx_info, uint32 msg_id) { const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; struct Flexcan_Ip_MsbuffCodeStatusType cs; Flexcan_Ip_StatusType eResult; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; long unsigned int _6; _Bool _7; long unsigned int _8; long unsigned int _9; _10; _Bool _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; Flexcan_Ip_StatusType _39; : # DEBUG BEGIN_STMT eResult_17 = 0; # DEBUG eResult => eResult_17 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = (int) instance_18(D); base_20 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_20 # DEBUG BEGIN_STMT _2 = (int) instance_18(D); state_21 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_21 # DEBUG BEGIN_STMT _3 = instance_18(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = rx_info_23(D) != 0B; DevAssert (_4); # DEBUG BEGIN_STMT _5 = state_21->bIsLegacyFifoEn; _6 = state_21->u32MaxMbNum; _7 = FlexCAN_IsMbOutOfRange (base_20, mb_idx_25(D), _5, _6); if (_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_38 = 4; # DEBUG eResult => eResult_38 goto ; [INV] : # DEBUG BEGIN_STMT _8 = (long unsigned int) mb_idx_25(D); FlexCAN_ClearMsgBuffIntStatusFlag (base_20, _8); # DEBUG BEGIN_STMT _9 = rx_info_23(D)->data_length; cs.dataLen = _9; # DEBUG BEGIN_STMT _10 = rx_info_23(D)->msg_id_type; cs.msgIdType = _10; # DEBUG BEGIN_STMT _11 = rx_info_23(D)->fd_enable; cs.fd_enable = _11; # DEBUG BEGIN_STMT cs.code = 15; # DEBUG BEGIN_STMT _12 = (long unsigned int) mb_idx_25(D); FlexCAN_SetRxMsgBuff (base_20, _12, &cs, msg_id_32(D)); # DEBUG BEGIN_STMT cs.code = 0; # DEBUG BEGIN_STMT _13 = (long unsigned int) mb_idx_25(D); FlexCAN_SetRxMsgBuff (base_20, _13, &cs, msg_id_32(D)); # DEBUG BEGIN_STMT cs.code = 4; # DEBUG BEGIN_STMT _14 = (long unsigned int) mb_idx_25(D); FlexCAN_SetRxMsgBuff (base_20, _14, &cs, msg_id_32(D)); : # eResult_15 = PHI # DEBUG eResult => eResult_15 # DEBUG BEGIN_STMT _39 = eResult_15; cs ={v} {CLOBBER}; return _39; } FlexCAN_Ip_Send (uint8 instance, uint8 mb_idx, const struct Flexcan_Ip_DataInfoType * tx_info, uint32 msg_id, const uint8 * mb_data) { const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; Flexcan_Ip_StatusType result; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; _Bool _6; _Bool _7; _Bool _8; long unsigned int _9; _Bool _10; Flexcan_Ip_StatusType _29; : # DEBUG BEGIN_STMT result_13 = 1; # DEBUG result => result_13 # DEBUG BEGIN_STMT _1 = (int) instance_14(D); base_16 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_16 # DEBUG BEGIN_STMT _2 = (int) instance_14(D); state_17 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_17 # DEBUG BEGIN_STMT _3 = instance_14(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = tx_info_19(D) != 0B; DevAssert (_4); # DEBUG BEGIN_STMT _5 = FlexCAN_IsListenOnlyModeEnabled (base_16); _6 = ~_5; if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_26 = FlexCAN_StartSendData (instance_14(D), mb_idx_22(D), tx_info_19(D), msg_id_23(D), mb_data_24(D)); # DEBUG result => result_26 # DEBUG BEGIN_STMT if (result_26 == 0) goto ; [INV] else goto ; [INV] : _7 = tx_info_19(D)->is_polling; _8 = ~_7; if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = (long unsigned int) mb_idx_22(D); _10 = state_17->isIntActive; result_28 = FlexCAN_SetMsgBuffIntCmd (base_16, instance_14(D), _9, 1, _10); # DEBUG result => result_28 : # result_11 = PHI # DEBUG result => result_11 # DEBUG BEGIN_STMT _29 = result_11; return _29; } FlexCAN_Ip_Init_Privileged (uint8 Flexcan_Ip_u8Instance, struct Flexcan_Ip_StateType * Flexcan_Ip_pState, const struct Flexcan_Ip_ConfigType * Flexcan_Ip_pData) { uint32 i; struct FLEXCAN_Type * pBase; Flexcan_Ip_StatusType eResult; int _1; _Bool _2; _Bool _3; _Bool _4; _Bool _5; long unsigned int _6; long unsigned int _7; const struct Flexcan_Ip_TimeSegmentType * _8; _Bool _9; const struct Flexcan_Ip_TimeSegmentType * _10; long unsigned int _11; long unsigned int _12; _Bool _13; const struct Flexcan_Ip_TimeSegmentType * _14; const struct Flexcan_Ip_TimeSegmentType * _15; const struct Flexcan_Ip_TimeSegmentType * _16; _17; _18; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct Flexcan_Ip_StateType *) _19; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct Flexcan_Ip_StateType *) _20; _Bool _21; long unsigned int _22; int _23; Flexcan_Ip_StatusType _73; : # DEBUG BEGIN_STMT eResult_31 = 0; # DEBUG eResult => eResult_31 # DEBUG BEGIN_STMT _1 = (int) Flexcan_Ip_u8Instance_32(D); pBase_34 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_34 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _2 = Flexcan_Ip_u8Instance_32(D) <= 5; DevAssert (_2); # DEBUG BEGIN_STMT _3 = Flexcan_Ip_pData_36(D) != 0B; DevAssert (_3); # DEBUG BEGIN_STMT eResult_39 = FlexCAN_InitController (pBase_34, Flexcan_Ip_pData_36(D)); # DEBUG eResult => eResult_39 # DEBUG BEGIN_STMT if (eResult_39 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = Flexcan_Ip_pData_36(D)->fd_enable; FlexCAN_EnableExtCbt (pBase_34, _4); # DEBUG BEGIN_STMT _5 = Flexcan_Ip_pData_36(D)->enhCbtEnable; if (_5 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_00 (); # DEBUG BEGIN_STMT _6 ={v} pBase_34->CTRL2; _7 = _6 | 8192; pBase_34->CTRL2 ={v} _7; # DEBUG BEGIN_STMT _8 = &Flexcan_Ip_pData_36(D)->bitrate; FlexCAN_SetEnhancedNominalTimeSegments (pBase_34, _8); # DEBUG BEGIN_STMT _9 = Flexcan_Ip_pData_36(D)->fd_enable; if (_9 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _10 = &Flexcan_Ip_pData_36(D)->bitrate_cbt; FlexCAN_SetEnhancedDataTimeSegments (pBase_34, _10); : # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_00 (); goto ; [INV] : # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_00 (); # DEBUG BEGIN_STMT _11 ={v} pBase_34->CTRL2; _12 = _11 & 4294959103; pBase_34->CTRL2 ={v} _12; # DEBUG BEGIN_STMT _13 = Flexcan_Ip_pData_36(D)->fd_enable; if (_13 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _14 = &Flexcan_Ip_pData_36(D)->bitrate; FlexCAN_SetExtendedTimeSegments (pBase_34, _14); # DEBUG BEGIN_STMT _15 = &Flexcan_Ip_pData_36(D)->bitrate_cbt; FlexCAN_SetFDTimeSegments (pBase_34, _15); goto ; [INV] : # DEBUG BEGIN_STMT _16 = &Flexcan_Ip_pData_36(D)->bitrate; FlexCAN_SetTimeSegments (pBase_34, _16); : # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_00 (); : # DEBUG BEGIN_STMT _17 = Flexcan_Ip_pData_36(D)->flexcanMode; FlexCAN_SetOperationMode (pBase_34, _17); # DEBUG BEGIN_STMT eResult_54 = FlexCAN_EnterFreezeMode (pBase_34); # DEBUG eResult => eResult_54 # DEBUG BEGIN_STMT if (eResult_54 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT i_55 = 0; # DEBUG i => i_55 goto ; [INV] : # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->mbs[i_25].isPolling = 1; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->mbs[i_25].pMBmessage = 0B; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->mbs[i_25].state ={v} 0; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->mbs[i_25].time_stamp = 0; # DEBUG BEGIN_STMT i_72 = i_25 + 1; # DEBUG i => i_72 : # i_25 = PHI # DEBUG i => i_25 # DEBUG BEGIN_STMT if (i_25 <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->enhancedFifoOutput.isPolling = 1; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->enhancedFifoOutput.state ={v} 0; # DEBUG BEGIN_STMT _18 = Flexcan_Ip_pData_36(D)->transfer_type; Flexcan_Ip_pState_56(D)->transferType = _18; # DEBUG BEGIN_STMT _19 = Flexcan_Ip_pData_36(D)->Callback; Flexcan_Ip_pState_56(D)->callback = _19; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->callbackParam = 0B; # DEBUG BEGIN_STMT _20 = Flexcan_Ip_pData_36(D)->ErrorCallback; Flexcan_Ip_pState_56(D)->error_callback = _20; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->errorCallbackParam = 0B; # DEBUG BEGIN_STMT _21 = Flexcan_Ip_pData_36(D)->is_rx_fifo_needed; Flexcan_Ip_pState_56(D)->bIsLegacyFifoEn = _21; # DEBUG BEGIN_STMT _22 = Flexcan_Ip_pData_36(D)->max_num_mb; Flexcan_Ip_pState_56(D)->u32MaxMbNum = _22; # DEBUG BEGIN_STMT Flexcan_Ip_pState_56(D)->isIntActive = 1; # DEBUG BEGIN_STMT _23 = (int) Flexcan_Ip_u8Instance_32(D); g_flexcan_Ip_StatePtr[_23] = Flexcan_Ip_pState_56(D); : # eResult_24 = PHI # DEBUG eResult => eResult_24 # DEBUG BEGIN_STMT _73 = eResult_24; return _73; } FlexCAN_AbortRxTransfer (uint8 u8Instance, uint8 mb_idx) { volatile uint32 * flexcan_mb; uint32 flexcan_mb_config; uint32 val2; uint32 val1; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * pBase; int _1; int _2; int _3; _Bool _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; _Bool _9; long unsigned int _10; long unsigned int _11; : # DEBUG BEGIN_STMT _1 = (int) u8Instance_14(D); pBase_16 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_16 # DEBUG BEGIN_STMT _2 = (int) u8Instance_14(D); state_17 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_17 # DEBUG BEGIN_STMT val1_18 = 0; # DEBUG val1 => val1_18 # DEBUG BEGIN_STMT val2_19 = 0; # DEBUG val2 => val2_19 # DEBUG BEGIN_STMT flexcan_mb_config_20 = 0; # DEBUG flexcan_mb_config => flexcan_mb_config_20 # DEBUG BEGIN_STMT flexcan_mb_21 = 0B; # DEBUG flexcan_mb => flexcan_mb_21 # DEBUG BEGIN_STMT _3 = (int) mb_idx_22(D); state_17->mbs[_3].state ={v} 0; # DEBUG BEGIN_STMT _4 = state_17->bIsLegacyFifoEn; if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 ={v} pBase_16->CTRL2; _6 = _5 >> 24; val1_33 = _6 & 15; # DEBUG val1 => val1_33 # DEBUG BEGIN_STMT val2_35 = RxFifoOcuppiedLastMsgBuff (val1_33); # DEBUG val2 => val2_35 # DEBUG BEGIN_STMT _7 = (long unsigned int) mb_idx_22(D); if (val2_35 < _7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = (long unsigned int) mb_idx_22(D); flexcan_mb_37 = FlexCAN_GetMsgBuffRegion (pBase_16, _8); # DEBUG flexcan_mb => flexcan_mb_37 # DEBUG BEGIN_STMT flexcan_mb_config_38 ={v} *flexcan_mb_37; # DEBUG flexcan_mb_config => flexcan_mb_config_38 # DEBUG BEGIN_STMT flexcan_mb_config_39 = flexcan_mb_config_38 & 4043309055; # DEBUG flexcan_mb_config => flexcan_mb_config_39 # DEBUG BEGIN_STMT flexcan_mb_config_40 = flexcan_mb_config_39; # DEBUG flexcan_mb_config => flexcan_mb_config_40 # DEBUG BEGIN_STMT *flexcan_mb_37 ={v} flexcan_mb_config_40; # DEBUG BEGIN_STMT flexcan_mb_config_42 = flexcan_mb_config_40 & 4043309055; # DEBUG flexcan_mb_config => flexcan_mb_config_42 # DEBUG BEGIN_STMT flexcan_mb_config_43 = flexcan_mb_config_42 | 67108864; # DEBUG flexcan_mb_config => flexcan_mb_config_43 # DEBUG BEGIN_STMT *flexcan_mb_37 ={v} flexcan_mb_config_43; : # DEBUG BEGIN_STMT if (mb_idx_22(D) == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = state_17->isIntActive; FLEXCAN_ClearMsgBuffIntCmd (pBase_16, u8Instance_14(D), 5, _9); goto ; [INV] : # DEBUG BEGIN_STMT _10 = (long unsigned int) mb_idx_22(D); flexcan_mb_25 = FlexCAN_GetMsgBuffRegion (pBase_16, _10); # DEBUG flexcan_mb => flexcan_mb_25 # DEBUG BEGIN_STMT flexcan_mb_config_26 ={v} *flexcan_mb_25; # DEBUG flexcan_mb_config => flexcan_mb_config_26 # DEBUG BEGIN_STMT flexcan_mb_config_27 = flexcan_mb_config_26 & 4043309055; # DEBUG flexcan_mb_config => flexcan_mb_config_27 # DEBUG BEGIN_STMT flexcan_mb_config_28 = flexcan_mb_config_27; # DEBUG flexcan_mb_config => flexcan_mb_config_28 # DEBUG BEGIN_STMT *flexcan_mb_25 ={v} flexcan_mb_config_28; # DEBUG BEGIN_STMT flexcan_mb_config_30 = flexcan_mb_config_28 & 4043309055; # DEBUG flexcan_mb_config => flexcan_mb_config_30 # DEBUG BEGIN_STMT flexcan_mb_config_31 = flexcan_mb_config_30 | 67108864; # DEBUG flexcan_mb_config => flexcan_mb_config_31 # DEBUG BEGIN_STMT *flexcan_mb_25 ={v} flexcan_mb_config_31; : # DEBUG BEGIN_STMT _11 = (long unsigned int) mb_idx_22(D); FlexCAN_ClearMsgBuffIntStatusFlag (pBase_16, _11); return; } FlexCAN_AbortTxTransfer (uint8 u8Instance, uint8 mb_idx) { volatile uint32 * flexcan_mb; uint32 uS2Ticks; uint32 flexcan_mb_config; uint32 timeElapsed; uint32 timeStart; Flexcan_Ip_StatusType result; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * pBase; int _1; int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; unsigned char _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; int _12; long unsigned int _42; Flexcan_Ip_StatusType _50; : # DEBUG BEGIN_STMT _1 = (int) u8Instance_19(D); pBase_21 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_21 # DEBUG BEGIN_STMT _2 = (int) u8Instance_19(D); state_22 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_22 # DEBUG BEGIN_STMT result_23 = 0; # DEBUG result => result_23 # DEBUG BEGIN_STMT timeStart = 0; # DEBUG BEGIN_STMT timeElapsed_25 = 0; # DEBUG timeElapsed => timeElapsed_25 # DEBUG BEGIN_STMT flexcan_mb_config_26 = 0; # DEBUG flexcan_mb_config => flexcan_mb_config_26 # DEBUG BEGIN_STMT uS2Ticks_27 = 0; # DEBUG uS2Ticks => uS2Ticks_27 # DEBUG BEGIN_STMT flexcan_mb_28 = 0B; # DEBUG flexcan_mb => flexcan_mb_28 # DEBUG BEGIN_STMT _3 = (long unsigned int) mb_idx_29(D); flexcan_mb_31 = FlexCAN_GetMsgBuffRegion (pBase_21, _3); # DEBUG flexcan_mb => flexcan_mb_31 # DEBUG BEGIN_STMT flexcan_mb_config_32 ={v} *flexcan_mb_31; # DEBUG flexcan_mb_config => flexcan_mb_config_32 # DEBUG BEGIN_STMT flexcan_mb_config_33 = flexcan_mb_config_32 & 4043309055; # DEBUG flexcan_mb_config => flexcan_mb_config_33 # DEBUG BEGIN_STMT flexcan_mb_config_34 = flexcan_mb_config_33 | 150994944; # DEBUG flexcan_mb_config => flexcan_mb_config_34 # DEBUG BEGIN_STMT *flexcan_mb_31 ={v} flexcan_mb_config_34; # DEBUG BEGIN_STMT uS2Ticks_37 = OsIf_MicrosToTicks (100, 0); # DEBUG uS2Ticks => uS2Ticks_37 # DEBUG BEGIN_STMT _4 = OsIf_GetCounter (0); timeStart = _4; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT _42 = OsIf_GetElapsed (&timeStart, 0); timeElapsed_43 = _42 + timeElapsed_16; # DEBUG timeElapsed => timeElapsed_43 # DEBUG BEGIN_STMT if (timeElapsed_43 >= uS2Ticks_37) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_44 = 3; # DEBUG result => result_44 # DEBUG BEGIN_STMT goto ; [INV] : # timeElapsed_16 = PHI # DEBUG timeElapsed => timeElapsed_16 # DEBUG BEGIN_STMT _5 = (long unsigned int) mb_idx_29(D); _6 = FlexCAN_GetBuffStatusFlag (pBase_21, _5); if (_6 == 0) goto ; [INV] else goto ; [INV] : # result_13 = PHI # DEBUG result => result_13 # DEBUG BEGIN_STMT if (result_13 != 3) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT flexcan_mb_config_45 ={v} *flexcan_mb_31; # DEBUG flexcan_mb_config => flexcan_mb_config_45 # DEBUG BEGIN_STMT _7 = flexcan_mb_config_45 >> 24; _8 = _7 & 15; if (_8 == 8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_46 = 5; # DEBUG result => result_46 : # result_14 = PHI # DEBUG result => result_14 # DEBUG BEGIN_STMT _9 = flexcan_mb_config_45 >> 24; _10 = _9 & 15; if (_10 == 9) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_47 = 0; # DEBUG result => result_47 : # result_15 = PHI # DEBUG result => result_15 # DEBUG BEGIN_STMT _11 = (long unsigned int) mb_idx_29(D); FlexCAN_ClearMsgBuffIntStatusFlag (pBase_21, _11); # DEBUG BEGIN_STMT _12 = (int) mb_idx_29(D); state_22->mbs[_12].state ={v} 0; # DEBUG BEGIN_STMT _50 = result_15; timeStart ={v} {CLOBBER}; return _50; } FlexCAN_IRQHandlerEnhancedRxFIFO (uint8 instance, uint32 intType) { struct Flexcan_Ip_MsgBuffType data; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; _3; struct Flexcan_Ip_MsgBuffType * _4; struct Flexcan_Ip_MsgBuffType * _5; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _6; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _7; _8; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _9; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _10; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _11; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _12; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _13; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _14; : # DEBUG BEGIN_STMT _1 = (int) instance_18(D); base_20 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_20 # DEBUG BEGIN_STMT _2 = (int) instance_18(D); state_21 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_21 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT switch (intType_22(D)) [INV], case 28: [INV], case 29: [INV], case 30: [INV], case 31: [INV]> : : # DEBUG BEGIN_STMT _3 ={v} state_21->enhancedFifoOutput.state; if (_3 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = state_21->enhancedFifoOutput.pMBmessage; if (_4 == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_21->enhancedFifoOutput.pMBmessage = &data; : # DEBUG BEGIN_STMT _5 = state_21->enhancedFifoOutput.pMBmessage; FlexCAN_ReadEnhancedRxFifo (base_20, _5); # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_20, intType_22(D)); # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_20, 29); # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_20, 30); # DEBUG BEGIN_STMT state_21->enhancedFifoOutput.state ={v} 0; # DEBUG BEGIN_STMT _6 = state_21->callback; if (_6 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = state_21->callback; _7 (instance_18(D), 5, 255, state_21); : # DEBUG BEGIN_STMT _8 ={v} state_21->enhancedFifoOutput.state; if (_8 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_CompleteRxMessageEnhancedFifoData (instance_18(D)); goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_20, intType_22(D)); # DEBUG BEGIN_STMT _9 = state_21->callback; if (_9 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _10 = state_21->callback; _10 (instance_18(D), 6, 255, state_21); goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_20, intType_22(D)); # DEBUG BEGIN_STMT _11 = state_21->callback; if (_11 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _12 = state_21->callback; _12 (instance_18(D), 7, 255, state_21); goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_20, intType_22(D)); # DEBUG BEGIN_STMT _13 = state_21->callback; if (_13 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _14 = state_21->callback; _14 (instance_18(D), 8, 255, state_21); : : data ={v} {CLOBBER}; return; } FlexCAN_ProcessIRQHandlerEnhancedRxFIFO (uint8 u8Instance, boolean bIsSpuriousIntPrevious) { boolean bIsSpuriousInt; uint32 u32intType; const struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; unsigned char _3; unsigned char _4; _Bool _5; _Bool _6; boolean _20; : # DEBUG BEGIN_STMT _1 = (int) u8Instance_12(D); base_14 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_14 # DEBUG BEGIN_STMT _2 = (int) u8Instance_12(D); state_15 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_15 # DEBUG BEGIN_STMT u32intType_16 = 0; # DEBUG u32intType => u32intType_16 # DEBUG BEGIN_STMT bIsSpuriousInt_18 = bIsSpuriousIntPrevious_17(D); # DEBUG bIsSpuriousInt => bIsSpuriousInt_18 # DEBUG BEGIN_STMT u32intType_19 = 31; # DEBUG u32intType => u32intType_19 goto ; [INV] : # DEBUG BEGIN_STMT _3 = FlexCAN_GetEnhancedRxFIFOStatusFlag (base_14, u32intType_7); if (_3 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = FlexCAN_GetEnhancedRxFIFOIntStatusFlag (base_14, u32intType_7); if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerEnhancedRxFIFO (u8Instance_12(D), u32intType_7); # DEBUG BEGIN_STMT bIsSpuriousInt_25 = 0; # DEBUG bIsSpuriousInt => bIsSpuriousInt_25 goto ; [INV] : # DEBUG BEGIN_STMT if (bIsSpuriousInt_9 != 0) goto ; [INV] else goto ; [INV] : _5 = state_15->enhancedFifoOutput.isPolling; _6 = ~_5; if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearEnhancedRxFifoIntStatusFlag (base_14, u32intType_7); : # bIsSpuriousInt_8 = PHI # DEBUG bIsSpuriousInt => bIsSpuriousInt_8 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT u32intType_26 = u32intType_7 + 4294967295; # DEBUG u32intType => u32intType_26 : # u32intType_7 = PHI # bIsSpuriousInt_9 = PHI # DEBUG bIsSpuriousInt => bIsSpuriousInt_9 # DEBUG u32intType => u32intType_7 # DEBUG BEGIN_STMT if (u32intType_7 > 27) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _20 = bIsSpuriousInt_9; return _20; } FlexCAN_ProcessSpuriousInterruptMB (uint8 instance, uint32 startMbIdx, uint32 endMbIdx) { uint32 u32MbHandle; uint32 mb_idx; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; unsigned char _3; unsigned char _4; _Bool _5; _Bool _6; _Bool _7; _8; : # DEBUG BEGIN_STMT _1 = (int) instance_13(D); base_15 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_15 # DEBUG BEGIN_STMT _2 = (int) instance_13(D); state_16 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_16 # DEBUG BEGIN_STMT mb_idx_17 = 0; # DEBUG mb_idx => mb_idx_17 # DEBUG BEGIN_STMT u32MbHandle_18 = 0; # DEBUG u32MbHandle => u32MbHandle_18 # DEBUG BEGIN_STMT mb_idx_20 = startMbIdx_19(D); # DEBUG mb_idx => mb_idx_20 goto ; [INV] : # DEBUG BEGIN_STMT _3 = FlexCAN_GetBuffStatusFlag (base_15, mb_idx_9); if (_3 != 0) goto ; [INV] else goto ; [INV] : _4 = FlexCAN_GetBuffStatusImask (base_15, mb_idx_9); if (_4 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT u32MbHandle_24 = mb_idx_9; # DEBUG u32MbHandle => u32MbHandle_24 # DEBUG BEGIN_STMT _5 = state_16->bIsLegacyFifoEn; if (_5 != 0) goto ; [INV] else goto ; [INV] : if (mb_idx_9 <= 7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT u32MbHandle_25 = 0; # DEBUG u32MbHandle => u32MbHandle_25 : # u32MbHandle_10 = PHI # DEBUG u32MbHandle => u32MbHandle_10 # DEBUG BEGIN_STMT _6 = state_16->mbs[u32MbHandle_10].isPolling; _7 = ~_6; if (_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_15, mb_idx_9); # DEBUG BEGIN_STMT _8 ={v} state_16->mbs[u32MbHandle_10].state; if (_8 == 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_16->mbs[u32MbHandle_10].state ={v} 0; # DEBUG BEGIN_STMT state_16->mbs[u32MbHandle_10].isPolling = 1; : # DEBUG BEGIN_STMT mb_idx_29 = mb_idx_9 + 1; # DEBUG mb_idx => mb_idx_29 : # mb_idx_9 = PHI # DEBUG mb_idx => mb_idx_9 # DEBUG BEGIN_STMT if (mb_idx_9 <= endMbIdx_21(D)) goto ; [INV] else goto ; [INV] : return; } FlexCAN_IRQHandlerRxFIFO (uint8 instance, uint32 mb_idx) { struct Flexcan_Ip_MsgBuffType data; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; struct Flexcan_Ip_MsgBuffType * _3; _4; struct Flexcan_Ip_MsgBuffType * _5; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _6; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _7; _8; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _9; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _10; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _11; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _12; : # DEBUG BEGIN_STMT _1 = (int) instance_16(D); base_18 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_18 # DEBUG BEGIN_STMT _2 = (int) instance_16(D); state_19 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_19 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _3 = state_19->mbs[0].pMBmessage; if (_3 == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_19->mbs[0].pMBmessage = &data; : # DEBUG BEGIN_STMT switch (mb_idx_21(D)) [INV], case 5: [INV], case 6: [INV], case 7: [INV]> : : # DEBUG BEGIN_STMT _4 ={v} state_19->mbs[0].state; if (_4 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = state_19->mbs[0].pMBmessage; FlexCAN_ReadRxFifo (base_18, _5); # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_18, mb_idx_21(D)); # DEBUG BEGIN_STMT state_19->mbs[0].state ={v} 0; # DEBUG BEGIN_STMT _6 = state_19->callback; if (_6 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = state_19->callback; _7 (instance_16(D), 1, 0, state_19); : # DEBUG BEGIN_STMT _8 ={v} state_19->mbs[0].state; if (_8 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_19->mbs[0].isPolling = 1; # DEBUG BEGIN_STMT FlexCAN_CompleteRxMessageFifoData (instance_16(D)); goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_18, mb_idx_21(D)); # DEBUG BEGIN_STMT _9 = state_19->callback; if (_9 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _10 = state_19->callback; _10 (instance_16(D), 2, 0, state_19); goto ; [INV] : : # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_18, mb_idx_21(D)); # DEBUG BEGIN_STMT _11 = state_19->callback; if (_11 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _12 = state_19->callback; _12 (instance_16(D), 3, 0, state_19); : : data ={v} {CLOBBER}; return; } FlexCAN_IRQHandlerTxMB (uint8 u8Instance, uint32 u32MbIdx) { boolean bCurrentIntStat; struct Flexcan_Ip_MsgBuffType mb; struct Flexcan_Ip_StateType * pState; struct FLEXCAN_Type * pBase; int _1; int _2; _Bool _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _9; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _10; _11; _Bool _12; _Bool _13; _Bool _14; _Bool _15; _Bool _16; _Bool _17; : # DEBUG BEGIN_STMT _1 = (int) u8Instance_21(D); pBase_23 = g_Flexcan_Ip_aBase[_1]; # DEBUG pBase => pBase_23 # DEBUG BEGIN_STMT _2 = (int) u8Instance_21(D); pState_24 = g_flexcan_Ip_StatePtr[_2]; # DEBUG pState => pState_24 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT bCurrentIntStat_25 = 0; # DEBUG bCurrentIntStat => bCurrentIntStat_25 # DEBUG BEGIN_STMT _3 = pState_24->mbs[u32MbIdx_26(D)].isRemote; if (_3 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_LockRxMsgBuff (pBase_23, u32MbIdx_26(D)); # DEBUG BEGIN_STMT FlexCAN_GetMsgBuff (pBase_23, u32MbIdx_26(D), &mb); # DEBUG BEGIN_STMT FlexCAN_UnlockRxMsgBuff (pBase_23); # DEBUG BEGIN_STMT _4 = mb.time_stamp; pState_24->mbs[u32MbIdx_26(D)].time_stamp = _4; # DEBUG BEGIN_STMT _5 = mb.cs; _6 = _5 >> 24; _7 = _6 & 15; if (_7 == 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (pBase_23, u32MbIdx_26(D)); goto ; [INV] : # DEBUG BEGIN_STMT _8 = FlexCAN_GetMsgBuffTimestamp (pBase_23, u32MbIdx_26(D)); pState_24->mbs[u32MbIdx_26(D)].time_stamp = _8; # DEBUG BEGIN_STMT FlexCAN_UnlockRxMsgBuff (pBase_23); # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (pBase_23, u32MbIdx_26(D)); : # DEBUG BEGIN_STMT pState_24->mbs[u32MbIdx_26(D)].state ={v} 0; # DEBUG BEGIN_STMT bCurrentIntStat_37 = pState_24->mbs[u32MbIdx_26(D)].isPolling; # DEBUG bCurrentIntStat => bCurrentIntStat_37 # DEBUG BEGIN_STMT _9 = pState_24->callback; if (_9 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _10 = pState_24->callback; _10 (u8Instance_21(D), 4, u32MbIdx_26(D), pState_24); : # DEBUG BEGIN_STMT _11 ={v} pState_24->mbs[u32MbIdx_26(D)].state; if (_11 == 0) goto ; [INV] else goto ; [INV] : _12 = pState_24->mbs[u32MbIdx_26(D)].isPolling; _13 = ~_12; if (_13 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pState_24->mbs[u32MbIdx_26(D)].isPolling = 1; # DEBUG BEGIN_STMT _14 = pState_24->isIntActive; FlexCAN_SetMsgBuffIntCmd (pBase_23, u8Instance_21(D), u32MbIdx_26(D), 0, _14); goto ; [INV] : # DEBUG BEGIN_STMT _15 = ~bCurrentIntStat_37; if (_15 != 0) goto ; [INV] else goto ; [INV] : _16 = pState_24->mbs[u32MbIdx_26(D)].isPolling; if (_16 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _17 = pState_24->isIntActive; FlexCAN_SetMsgBuffIntCmd (pBase_23, u8Instance_21(D), u32MbIdx_26(D), 0, _17); : # DEBUG BEGIN_STMT mb ={v} {CLOBBER}; return; } FlexCAN_IRQHandlerRxMB (uint8 instance, uint32 mb_idx) { boolean bCurrentIntStat; struct Flexcan_Ip_MsgBuffType data; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; struct Flexcan_Ip_MsgBuffType * _3; struct Flexcan_Ip_MsgBuffType * _4; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _5; void (*) (uint8, Flexcan_Ip_EventType, uint32, const struct FlexCANState *) _6; _7; _Bool _8; _Bool _9; _Bool _10; _Bool _11; _Bool _12; _Bool _13; : # DEBUG BEGIN_STMT _1 = (int) instance_17(D); base_19 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_19 # DEBUG BEGIN_STMT _2 = (int) instance_17(D); state_20 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_20 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT bCurrentIntStat_21 = 0; # DEBUG bCurrentIntStat => bCurrentIntStat_21 # DEBUG BEGIN_STMT _3 = state_20->mbs[mb_idx_22(D)].pMBmessage; if (_3 == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_20->mbs[mb_idx_22(D)].pMBmessage = &data; : # DEBUG BEGIN_STMT FlexCAN_LockRxMsgBuff (base_19, mb_idx_22(D)); # DEBUG BEGIN_STMT _4 = state_20->mbs[mb_idx_22(D)].pMBmessage; FlexCAN_GetMsgBuff (base_19, mb_idx_22(D), _4); # DEBUG BEGIN_STMT FlexCAN_ClearMsgBuffIntStatusFlag (base_19, mb_idx_22(D)); # DEBUG BEGIN_STMT FlexCAN_UnlockRxMsgBuff (base_19); # DEBUG BEGIN_STMT state_20->mbs[mb_idx_22(D)].state ={v} 0; # DEBUG BEGIN_STMT bCurrentIntStat_29 = state_20->mbs[mb_idx_22(D)].isPolling; # DEBUG bCurrentIntStat => bCurrentIntStat_29 # DEBUG BEGIN_STMT _5 = state_20->callback; if (_5 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = state_20->callback; _6 (instance_17(D), 0, mb_idx_22(D), state_20); : # DEBUG BEGIN_STMT _7 ={v} state_20->mbs[mb_idx_22(D)].state; if (_7 == 0) goto ; [INV] else goto ; [INV] : _8 = state_20->mbs[mb_idx_22(D)].isPolling; _9 = ~_8; if (_9 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_20->mbs[mb_idx_22(D)].isPolling = 1; # DEBUG BEGIN_STMT _10 = state_20->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_19, instance_17(D), mb_idx_22(D), 0, _10); goto ; [INV] : # DEBUG BEGIN_STMT _11 = ~bCurrentIntStat_29; if (_11 != 0) goto ; [INV] else goto ; [INV] : _12 = state_20->mbs[mb_idx_22(D)].isPolling; if (_12 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = state_20->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_19, instance_17(D), mb_idx_22(D), 0, _13); : # DEBUG BEGIN_STMT data ={v} {CLOBBER}; return; } FlexCAN_StartRxMessageFifoData (uint8 instance, struct Flexcan_Ip_MsgBuffType * data) { Flexcan_Ip_StatusType eResult; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; _Bool _1; int _2; int _3; _Bool _4; _Bool _5; _6; _7; _8; _Bool _9; _Bool _10; _Bool _11; Flexcan_Ip_StatusType _33; : # DEBUG BEGIN_STMT base_15 = 0B; # DEBUG base => base_15 # DEBUG BEGIN_STMT state_16 = 0B; # DEBUG state => state_16 # DEBUG BEGIN_STMT eResult_17 = 0; # DEBUG eResult => eResult_17 # DEBUG BEGIN_STMT _1 = instance_18(D) <= 5; DevAssert (_1); # DEBUG BEGIN_STMT _2 = (int) instance_18(D); base_21 = g_Flexcan_Ip_aBase[_2]; # DEBUG base => base_21 # DEBUG BEGIN_STMT _3 = (int) instance_18(D); state_22 = g_flexcan_Ip_StatePtr[_3]; # DEBUG state => state_22 # DEBUG BEGIN_STMT _4 = state_22->bIsLegacyFifoEn; _5 = ~_4; if (_5 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_32 = 1; # DEBUG eResult => eResult_32 goto ; [INV] : # DEBUG BEGIN_STMT _6 ={v} state_22->mbs[0].state; if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_31 = 2; # DEBUG eResult => eResult_31 goto ; [INV] : # DEBUG BEGIN_STMT state_22->mbs[0].state ={v} 1; # DEBUG BEGIN_STMT _7 = state_22->transferType; if (_7 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_22->mbs[0].isPolling = 1; : # DEBUG BEGIN_STMT state_22->mbs[0].pMBmessage = data_25(D); # DEBUG BEGIN_STMT _8 = state_22->transferType; if (_8 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_22->mbs[0].isPolling = 0; # DEBUG BEGIN_STMT _9 = state_22->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_21, instance_18(D), 6, 1, _9); # DEBUG BEGIN_STMT _10 = state_22->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_21, instance_18(D), 7, 1, _10); # DEBUG BEGIN_STMT _11 = state_22->isIntActive; FlexCAN_SetMsgBuffIntCmd (base_21, instance_18(D), 5, 1, _11); : # eResult_12 = PHI # DEBUG eResult => eResult_12 # DEBUG BEGIN_STMT _33 = eResult_12; return _33; } FlexCAN_StartSendData (uint8 Flexcan_Ip_u8Instance, uint8 mb_idx, const struct Flexcan_Ip_DataInfoType * tx_info, uint32 msg_id, const uint8 * mb_data) { struct FLEXCAN_Type * base; struct Flexcan_Ip_StateType * state; struct Flexcan_Ip_MsbuffCodeStatusType cs; Flexcan_Ip_StatusType eResult; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; long unsigned int _6; _Bool _7; int _8; _9; long unsigned int _10; int _11; int _12; int _13; _Bool _14; int _15; _Bool _16; long unsigned int _17; _18; _Bool _19; unsigned char _20; _Bool _21; _Bool _22; long unsigned int _23; Flexcan_Ip_StatusType _54; : # DEBUG BEGIN_STMT eResult_27 = 0; # DEBUG eResult => eResult_27 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = (int) Flexcan_Ip_u8Instance_28(D); state_30 = g_flexcan_Ip_StatePtr[_1]; # DEBUG state => state_30 # DEBUG BEGIN_STMT _2 = (int) Flexcan_Ip_u8Instance_28(D); base_31 = g_Flexcan_Ip_aBase[_2]; # DEBUG base => base_31 # DEBUG BEGIN_STMT _3 = Flexcan_Ip_u8Instance_28(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = tx_info_33(D) != 0B; DevAssert (_4); # DEBUG BEGIN_STMT _5 = state_30->bIsLegacyFifoEn; _6 = state_30->u32MaxMbNum; _7 = FlexCAN_IsMbOutOfRange (base_31, mb_idx_35(D), _5, _6); if (_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_53 = 4; # DEBUG eResult => eResult_53 goto ; [INV] : # DEBUG BEGIN_STMT _8 = (int) mb_idx_35(D); _9 ={v} state_30->mbs[_8].state; if (_9 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_52 = 2; # DEBUG eResult => eResult_52 goto ; [INV] : # DEBUG BEGIN_STMT _10 = (long unsigned int) mb_idx_35(D); FlexCAN_ClearMsgBuffIntStatusFlag (base_31, _10); # DEBUG BEGIN_STMT _11 = (int) mb_idx_35(D); state_30->mbs[_11].state ={v} 2; # DEBUG BEGIN_STMT _12 = (int) mb_idx_35(D); state_30->mbs[_12].time_stamp = 0; # DEBUG BEGIN_STMT _13 = (int) mb_idx_35(D); _14 = tx_info_33(D)->is_polling; state_30->mbs[_13].isPolling = _14; # DEBUG BEGIN_STMT _15 = (int) mb_idx_35(D); _16 = tx_info_33(D)->is_remote; state_30->mbs[_15].isRemote = _16; # DEBUG BEGIN_STMT _17 = tx_info_33(D)->data_length; cs.dataLen = _17; # DEBUG BEGIN_STMT _18 = tx_info_33(D)->msg_id_type; cs.msgIdType = _18; # DEBUG BEGIN_STMT _19 = tx_info_33(D)->fd_enable; cs.fd_enable = _19; # DEBUG BEGIN_STMT _20 = tx_info_33(D)->fd_padding; cs.fd_padding = _20; # DEBUG BEGIN_STMT _21 = tx_info_33(D)->enable_brs; cs.enable_brs = _21; # DEBUG BEGIN_STMT _22 = tx_info_33(D)->is_remote; if (_22 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT cs.code = 28; goto ; [INV] : # DEBUG BEGIN_STMT cs.code = 12; : # DEBUG BEGIN_STMT _23 = (long unsigned int) mb_idx_35(D); FlexCAN_SetTxMsgBuff (base_31, _23, &cs, msg_id_49(D), mb_data_50(D), 0); : # eResult_24 = PHI # DEBUG eResult => eResult_24 # DEBUG BEGIN_STMT _54 = eResult_24; cs ={v} {CLOBBER}; return _54; } FlexCAN_StartRxMessageBufferData (uint8 instance, uint8 mb_idx, struct Flexcan_Ip_MsgBuffType * data, boolean isPolling) { struct Flexcan_Ip_StateType * state; const struct FLEXCAN_Type * base; Flexcan_Ip_StatusType result; int _1; int _2; _Bool _3; _Bool _4; long unsigned int _5; _Bool _6; int _7; _8; int _9; int _10; int _11; Flexcan_Ip_StatusType _29; : # DEBUG BEGIN_STMT result_14 = 0; # DEBUG result => result_14 # DEBUG BEGIN_STMT _1 = (int) instance_15(D); base_17 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_17 # DEBUG BEGIN_STMT _2 = (int) instance_15(D); state_18 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_18 # DEBUG BEGIN_STMT _3 = instance_15(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = state_18->bIsLegacyFifoEn; _5 = state_18->u32MaxMbNum; _6 = FlexCAN_IsMbOutOfRange (base_17, mb_idx_20(D), _4, _5); if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_28 = 4; # DEBUG result => result_28 goto ; [INV] : # DEBUG BEGIN_STMT _7 = (int) mb_idx_20(D); _8 ={v} state_18->mbs[_7].state; if (_8 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT result_27 = 2; # DEBUG result => result_27 goto ; [INV] : # DEBUG BEGIN_STMT _9 = (int) mb_idx_20(D); state_18->mbs[_9].state ={v} 1; # DEBUG BEGIN_STMT _10 = (int) mb_idx_20(D); state_18->mbs[_10].pMBmessage = data_23(D); # DEBUG BEGIN_STMT _11 = (int) mb_idx_20(D); state_18->mbs[_11].isPolling = isPolling_25(D); : # result_12 = PHI # DEBUG result => result_12 # DEBUG BEGIN_STMT _29 = result_12; return _29; } FlexCAN_ProccessLegacyRxFIFO (uint8 u8Instance, uint32 u32TimeoutMs) { uint32 u32intType; uint32 mS2Ticks; uint32 timeElapsed; uint32 timeStart; struct FLEXCAN_Type * pBase; struct Flexcan_Ip_StateType * pState; Flexcan_Ip_StatusType eResult; int _1; int _2; long unsigned int _3; long unsigned int _4; _5; unsigned char _6; _7; _8; _Bool _9; _Bool _10; _Bool _11; _12; int _13; long unsigned int _43; Flexcan_Ip_StatusType _52; : # DEBUG BEGIN_STMT eResult_25 = 0; # DEBUG eResult => eResult_25 # DEBUG BEGIN_STMT _1 = (int) u8Instance_26(D); pState_28 = g_flexcan_Ip_StatePtr[_1]; # DEBUG pState => pState_28 # DEBUG BEGIN_STMT _2 = (int) u8Instance_26(D); pBase_29 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_29 # DEBUG BEGIN_STMT timeStart = 0; # DEBUG BEGIN_STMT timeElapsed_31 = 0; # DEBUG timeElapsed => timeElapsed_31 # DEBUG BEGIN_STMT _3 = u32TimeoutMs_32(D) * 1000; mS2Ticks_34 = OsIf_MicrosToTicks (_3, 0); # DEBUG mS2Ticks => mS2Ticks_34 # DEBUG BEGIN_STMT u32intType_35 = 0; # DEBUG u32intType => u32intType_35 # DEBUG BEGIN_STMT _4 = OsIf_GetCounter (0); timeStart = _4; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT _5 = pState_28->transferType; if (_5 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT u32intType_38 = 7; # DEBUG u32intType => u32intType_38 goto ; [INV] : # DEBUG BEGIN_STMT _6 = FlexCAN_GetBuffStatusFlag (pBase_29, u32intType_17); if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerRxFIFO (u8Instance_26(D), u32intType_17); : # DEBUG BEGIN_STMT u32intType_41 = u32intType_17 + 4294967295; # DEBUG u32intType => u32intType_41 : # u32intType_17 = PHI # DEBUG u32intType => u32intType_17 # DEBUG BEGIN_STMT if (u32intType_17 > 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _43 = OsIf_GetElapsed (&timeStart, 0); timeElapsed_44 = _43 + timeElapsed_16; # DEBUG timeElapsed => timeElapsed_44 # DEBUG BEGIN_STMT if (timeElapsed_44 >= mS2Ticks_34) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_45 = 3; # DEBUG eResult => eResult_45 # DEBUG BEGIN_STMT goto ; [INV] : # timeElapsed_16 = PHI # DEBUG timeElapsed => timeElapsed_16 # DEBUG BEGIN_STMT _7 ={v} pState_28->mbs[0].state; if (_7 == 1) goto ; [INV] else goto ; [INV] : # eResult_14 = PHI # DEBUG eResult => eResult_14 # DEBUG BEGIN_STMT if (eResult_14 == 3) goto ; [INV] else goto ; [INV] : _8 = pState_28->transferType; if (_8 != 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = pState_28->isIntActive; FlexCAN_SetMsgBuffIntCmd (pBase_29, u8Instance_26(D), 5, 0, _9); # DEBUG BEGIN_STMT _10 = pState_28->isIntActive; FlexCAN_SetMsgBuffIntCmd (pBase_29, u8Instance_26(D), 6, 0, _10); # DEBUG BEGIN_STMT _11 = pState_28->isIntActive; FlexCAN_SetMsgBuffIntCmd (pBase_29, u8Instance_26(D), 7, 0, _11); : # DEBUG BEGIN_STMT _12 ={v} pState_28->mbs[0].state; _13 = (int) _12; switch (_13) [INV], case 0: [INV], case 1: [INV]> : : # DEBUG BEGIN_STMT pState_28->mbs[0].state ={v} 0; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT eResult_50 = 0; # DEBUG eResult => eResult_50 # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT eResult_51 = 1; # DEBUG eResult => eResult_51 # DEBUG BEGIN_STMT : # eResult_15 = PHI # DEBUG eResult => eResult_15 # DEBUG BEGIN_STMT _52 = eResult_15; timeStart ={v} {CLOBBER}; return _52; } FlexCAN_ProccessEnhancedRxFifo (uint8 u8Instance, uint32 u32TimeoutMs) { uint32 u32intType; uint32 mS2Ticks; uint32 timeElapsed; uint32 timeStart; struct FLEXCAN_Type * pBase; struct Flexcan_Ip_StateType * pState; Flexcan_Ip_StatusType eResult; int _1; int _2; long unsigned int _3; long unsigned int _4; _5; unsigned char _6; _7; _8; _9; int _10; long unsigned int _40; Flexcan_Ip_StatusType _47; : # DEBUG BEGIN_STMT eResult_22 = 0; # DEBUG eResult => eResult_22 # DEBUG BEGIN_STMT _1 = (int) u8Instance_23(D); pState_25 = g_flexcan_Ip_StatePtr[_1]; # DEBUG pState => pState_25 # DEBUG BEGIN_STMT _2 = (int) u8Instance_23(D); pBase_26 = g_Flexcan_Ip_aBase[_2]; # DEBUG pBase => pBase_26 # DEBUG BEGIN_STMT timeStart = 0; # DEBUG BEGIN_STMT timeElapsed_28 = 0; # DEBUG timeElapsed => timeElapsed_28 # DEBUG BEGIN_STMT _3 = u32TimeoutMs_29(D) * 1000; mS2Ticks_31 = OsIf_MicrosToTicks (_3, 0); # DEBUG mS2Ticks => mS2Ticks_31 # DEBUG BEGIN_STMT u32intType_32 = 0; # DEBUG u32intType => u32intType_32 # DEBUG BEGIN_STMT _4 = OsIf_GetCounter (0); timeStart = _4; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT _5 = pState_25->transferType; if (_5 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT u32intType_35 = 31; # DEBUG u32intType => u32intType_35 goto ; [INV] : # DEBUG BEGIN_STMT _6 = FlexCAN_GetEnhancedRxFIFOStatusFlag (pBase_26, u32intType_14); if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_IRQHandlerEnhancedRxFIFO (u8Instance_23(D), u32intType_14); : # DEBUG BEGIN_STMT u32intType_38 = u32intType_14 + 4294967295; # DEBUG u32intType => u32intType_38 : # u32intType_14 = PHI # DEBUG u32intType => u32intType_14 # DEBUG BEGIN_STMT if (u32intType_14 > 27) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _40 = OsIf_GetElapsed (&timeStart, 0); timeElapsed_41 = _40 + timeElapsed_13; # DEBUG timeElapsed => timeElapsed_41 # DEBUG BEGIN_STMT if (timeElapsed_41 >= mS2Ticks_31) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_42 = 3; # DEBUG eResult => eResult_42 # DEBUG BEGIN_STMT goto ; [INV] : # timeElapsed_13 = PHI # DEBUG timeElapsed => timeElapsed_13 # DEBUG BEGIN_STMT _7 ={v} pState_25->enhancedFifoOutput.state; if (_7 == 1) goto ; [INV] else goto ; [INV] : # eResult_11 = PHI # DEBUG eResult => eResult_11 # DEBUG BEGIN_STMT if (eResult_11 == 3) goto ; [INV] else goto ; [INV] : _8 = pState_25->transferType; if (_8 != 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedRxFifoIntAll (pBase_26, 0); : # DEBUG BEGIN_STMT _9 ={v} pState_25->enhancedFifoOutput.state; _10 = (int) _9; switch (_10) [INV], case 0: [INV], case 1: [INV]> : : # DEBUG BEGIN_STMT pState_25->enhancedFifoOutput.state ={v} 0; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT eResult_45 = 0; # DEBUG eResult => eResult_45 # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT eResult_46 = 1; # DEBUG eResult => eResult_46 # DEBUG BEGIN_STMT : # eResult_12 = PHI # DEBUG eResult => eResult_12 # DEBUG BEGIN_STMT _47 = eResult_12; timeStart ={v} {CLOBBER}; return _47; } FlexCAN_StartRxMessageEnhancedFifoData (uint8 instance, struct Flexcan_Ip_MsgBuffType * data) { Flexcan_Ip_StatusType eResult; struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; _Bool _3; _4; _5; _Bool _6; _7; Flexcan_Ip_StatusType _24; : # DEBUG BEGIN_STMT _1 = (int) instance_11(D); base_13 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_13 # DEBUG BEGIN_STMT _2 = (int) instance_11(D); state_14 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_14 # DEBUG BEGIN_STMT eResult_15 = 0; # DEBUG eResult => eResult_15 # DEBUG BEGIN_STMT _3 = instance_11(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 ={v} state_14->enhancedFifoOutput.state; if (_4 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_23 = 2; # DEBUG eResult => eResult_23 goto ; [INV] : # DEBUG BEGIN_STMT state_14->enhancedFifoOutput.state ={v} 1; # DEBUG BEGIN_STMT state_14->enhancedFifoOutput.pMBmessage = data_18(D); # DEBUG BEGIN_STMT _5 = state_14->transferType; if (_5 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_14->enhancedFifoOutput.isPolling = 0; # DEBUG BEGIN_STMT _6 = state_14->isIntActive; if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetEnhancedRxFifoIntAll (base_13, 1); : # DEBUG BEGIN_STMT _7 = state_14->transferType; if (_7 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_14->enhancedFifoOutput.isPolling = 1; : # eResult_8 = PHI # DEBUG eResult => eResult_8 # DEBUG BEGIN_STMT _24 = eResult_8; return _24; } FlexCAN_CompleteRxMessageEnhancedFifoData (uint8 instance) { struct Flexcan_Ip_StateType * state; struct FLEXCAN_Type * base; int _1; int _2; _Bool _3; _Bool _4; _Bool _5; _Bool _6; : # DEBUG BEGIN_STMT _1 = (int) instance_8(D); base_10 = g_Flexcan_Ip_aBase[_1]; # DEBUG base => base_10 # DEBUG BEGIN_STMT _2 = (int) instance_8(D); state_11 = g_flexcan_Ip_StatePtr[_2]; # DEBUG state => state_11 # DEBUG BEGIN_STMT _3 = instance_8(D) <= 5; DevAssert (_3); # DEBUG BEGIN_STMT _4 = FlexCAN_IsEnhancedRxFifoAvailable (base_10); DevAssert (_4); # DEBUG BEGIN_STMT _5 = state_11->enhancedFifoOutput.isPolling; _6 = ~_5; if (_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT state_11->enhancedFifoOutput.isPolling = 1; # DEBUG BEGIN_STMT FlexCAN_SetEnhancedRxFifoIntAll (base_10, 0); : # DEBUG BEGIN_STMT state_11->enhancedFifoOutput.pMBmessage = 0B; # DEBUG BEGIN_STMT state_11->enhancedFifoOutput.state ={v} 0; return; } FlexCAN_InitController (struct FLEXCAN_Type * pBase, const struct Flexcan_Ip_ConfigType * Flexcan_Ip_pData) { Flexcan_Ip_StatusType eResult; _Bool _1; long unsigned int _2; long unsigned int _3; _Bool _4; _Bool _5; long unsigned int _6; _7; const struct Flexcan_Ip_PayloadSizeType * _8; long unsigned int _9; Flexcan_Ip_StatusType _44; : # DEBUG BEGIN_STMT eResult_15 = 0; # DEBUG eResult => eResult_15 # DEBUG BEGIN_STMT _1 = FlexCAN_IsEnabled (pBase_17(D)); if (_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_20 = FlexCAN_EnterFreezeMode (pBase_17(D)); # DEBUG eResult => eResult_20 # DEBUG BEGIN_STMT if (eResult_20 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eResult_22 = FlexCAN_Disable (pBase_17(D)); # DEBUG eResult => eResult_22 : # eResult_10 = PHI # DEBUG eResult => eResult_10 # DEBUG BEGIN_STMT if (eResult_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT SchM_Enter_Can_CAN_EXCLUSIVE_AREA_00 (); # DEBUG BEGIN_STMT _2 ={v} pBase_17(D)->MCR; _3 = _2 & 2147483647; pBase_17(D)->MCR ={v} _3; # DEBUG BEGIN_STMT SchM_Exit_Can_CAN_EXCLUSIVE_AREA_00 (); # DEBUG BEGIN_STMT eResult_27 = FlexCAN_Init (pBase_17(D)); # DEBUG eResult => eResult_27 # DEBUG BEGIN_STMT if (eResult_27 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_EnterFreezeMode (pBase_17(D)); # DEBUG BEGIN_STMT FlexCAN_Disable (pBase_17(D)); goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_DisableMemErrorDetection (pBase_17(D)); # DEBUG BEGIN_STMT _4 = Flexcan_Ip_pData_29(D)->fd_enable; _5 = Flexcan_Ip_pData_29(D)->bitRateSwitch; FlexCAN_SetFDEnabled (pBase_17(D), _4, _5); # DEBUG BEGIN_STMT _6 = Flexcan_Ip_pData_29(D)->ctrlOptions; FlexCAN_ConfigCtrlOptions (pBase_17(D), _6); # DEBUG BEGIN_STMT _7 = Flexcan_Ip_pData_29(D)->flexcanMode; if (_7 != 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_SetSelfReception (pBase_17(D), 0); : # DEBUG BEGIN_STMT eResult_34 = FlexCAN_InitRxFifo (pBase_17(D), Flexcan_Ip_pData_29(D)); # DEBUG eResult => eResult_34 # DEBUG BEGIN_STMT if (eResult_34 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_EnterFreezeMode (pBase_17(D)); # DEBUG BEGIN_STMT FlexCAN_Disable (pBase_17(D)); goto ; [INV] : # DEBUG BEGIN_STMT _8 = &Flexcan_Ip_pData_29(D)->payload; FlexCAN_SetPayloadSize (pBase_17(D), _8); # DEBUG BEGIN_STMT _9 = Flexcan_Ip_pData_29(D)->max_num_mb; eResult_37 = FlexCAN_SetMaxMsgBuffNum (pBase_17(D), _9); # DEBUG eResult => eResult_37 # DEBUG BEGIN_STMT if (eResult_37 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT FlexCAN_EnterFreezeMode (pBase_17(D)); # DEBUG BEGIN_STMT FlexCAN_Disable (pBase_17(D)); : # eResult_11 = PHI # DEBUG eResult => eResult_11 # DEBUG BEGIN_STMT _44 = eResult_11; return _44; } FlexCAN_InitRxFifo (struct FLEXCAN_Type * pBase, const struct Flexcan_Ip_ConfigType * Flexcan_Ip_pData) { Flexcan_Ip_StatusType eResult; _Bool _1; _2; long unsigned int _3; _Bool _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; Flexcan_Ip_StatusType _20; : # DEBUG BEGIN_STMT eResult_12 = 0; # DEBUG eResult => eResult_12 # DEBUG BEGIN_STMT _1 = Flexcan_Ip_pData_14(D)->is_rx_fifo_needed; if (_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _2 = Flexcan_Ip_pData_14(D)->num_id_filters; _3 = (long unsigned int) _2; eResult_17 = FlexCAN_EnableRxFifo (pBase_15(D), _3); # DEBUG eResult => eResult_17 : # eResult_8 = PHI # DEBUG eResult => eResult_8 # DEBUG BEGIN_STMT if (eResult_8 == 0) goto ; [INV] else goto ; [INV] : _4 = Flexcan_Ip_pData_14(D)->is_enhanced_rx_fifo_needed; if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = Flexcan_Ip_pData_14(D)->num_enhanced_std_id_filters; _6 = Flexcan_Ip_pData_14(D)->num_enhanced_ext_id_filters; _7 = Flexcan_Ip_pData_14(D)->num_enhanced_watermark; eResult_19 = FlexCAN_EnableEnhancedRxFifo (pBase_15(D), _5, _6, _7); # DEBUG eResult => eResult_19 : # eResult_9 = PHI # DEBUG eResult => eResult_9 # DEBUG BEGIN_STMT _20 = eResult_9; return _20; } FlexCAN_SetRegDefaultVal (struct FLEXCAN_Type * base) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; : # DEBUG BEGIN_STMT _1 = FlexCAN_IsEnhancedRxFifoAvailable (base_16(D)); if (_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT base_16(D)->ERFSR ={v} 4160749568; # DEBUG BEGIN_STMT base_16(D)->ERFIER ={v} 0; # DEBUG BEGIN_STMT base_16(D)->ERFCR ={v} 0; : # DEBUG BEGIN_STMT base_16(D)->FDCBT ={v} 0; # DEBUG BEGIN_STMT base_16(D)->FDCTRL ={v} 2147500288; # DEBUG BEGIN_STMT base_16(D)->ERRSR ={v} 851981; # DEBUG BEGIN_STMT base_16(D)->ERRIPPR ={v} 0; # DEBUG BEGIN_STMT base_16(D)->ERRIDPR ={v} 0; # DEBUG BEGIN_STMT base_16(D)->ERRIAR ={v} 0; # DEBUG BEGIN_STMT _2 ={v} base_16(D)->CTRL2; _3 = _2 | 536870912; base_16(D)->CTRL2 ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_16(D)->MECR; _5 = _4 & 2147483647; base_16(D)->MECR ={v} _5; # DEBUG BEGIN_STMT base_16(D)->MECR ={v} 786560; # DEBUG BEGIN_STMT _6 ={v} base_16(D)->MECR; _7 = _6 | 2147483648; base_16(D)->MECR ={v} _7; # DEBUG BEGIN_STMT _8 ={v} base_16(D)->CTRL2; _9 = _8 & 3758096383; base_16(D)->CTRL2 ={v} _9; # DEBUG BEGIN_STMT _10 = FlexCAN_GetMaxMbNum (base_16(D)); if (_10 > 64) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT base_16(D)->IFLAG3 ={v} 4294967295; # DEBUG BEGIN_STMT base_16(D)->IMASK3 ={v} 0; : # DEBUG BEGIN_STMT _11 = FlexCAN_GetMaxMbNum (base_16(D)); if (_11 > 32) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT base_16(D)->IFLAG2 ={v} 4294967295; # DEBUG BEGIN_STMT base_16(D)->IMASK2 ={v} 0; : # DEBUG BEGIN_STMT base_16(D)->IFLAG1 ={v} 4294967295; # DEBUG BEGIN_STMT base_16(D)->IMASK1 ={v} 0; # DEBUG BEGIN_STMT base_16(D)->CBT ={v} 0; # DEBUG BEGIN_STMT base_16(D)->CTRL2 ={v} 1048576; # DEBUG BEGIN_STMT base_16(D)->ESR1 ={v} 241670; # DEBUG BEGIN_STMT base_16(D)->ECR ={v} 0; # DEBUG BEGIN_STMT base_16(D)->TIMER ={v} 0; # DEBUG BEGIN_STMT base_16(D)->CTRL1 ={v} 0; # DEBUG BEGIN_STMT base_16(D)->EPRS ={v} 0; # DEBUG BEGIN_STMT base_16(D)->ENCBT ={v} 0; # DEBUG BEGIN_STMT base_16(D)->EDCBT ={v} 0; # DEBUG BEGIN_STMT base_16(D)->ETDC ={v} 0; # DEBUG BEGIN_STMT base_16(D)->MCR ={v} 3633315855; return; } FlexCAN_GetEnhancedRxFIFOIntStatusFlag (const struct FLEXCAN_Type * base, uint32 intFlag) { long unsigned int _1; unsigned char _2; int _3; int _4; long unsigned int _5; long unsigned int _6; unsigned char _7; int _8; int _9; long unsigned int _10; uint8 _14; : # DEBUG BEGIN_STMT _1 ={v} base_12(D)->ERFIER; _2 = (unsigned char) intFlag_13(D); _3 = (int) _2; _4 = _3 & 31; _5 = 1 << _4; _6 = _1 & _5; _7 = (unsigned char) intFlag_13(D); _8 = (int) _7; _9 = _8 & 31; _10 = _6 >> _9; _14 = (uint8) _10; return _14; } FlexCAN_ClearEnhancedRxFifoIntStatusFlag (struct FLEXCAN_Type * base, uint32 intFlag) { long unsigned int _1; : # DEBUG BEGIN_STMT _1 = 1 << intFlag_2(D); base_4(D)->ERFSR ={v} _1; return; } FlexCAN_GetEnhancedRxFIFOStatusFlag (const struct FLEXCAN_Type * base, uint32 intFlag) { long unsigned int _1; unsigned char _2; int _3; int _4; long unsigned int _5; long unsigned int _6; unsigned char _7; int _8; int _9; long unsigned int _10; uint8 _14; : # DEBUG BEGIN_STMT _1 ={v} base_12(D)->ERFSR; _2 = (unsigned char) intFlag_13(D); _3 = (int) _2; _4 = _3 & 31; _5 = 1 << _4; _6 = _1 & _5; _7 = (unsigned char) intFlag_13(D); _8 = (int) _7; _9 = _8 & 31; _10 = _6 >> _9; _14 = (uint8) _10; return _14; } FlexCAN_SetEnhancedRxFifoIntAll (struct FLEXCAN_Type * base, boolean enable) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; : # DEBUG BEGIN_STMT if (enable_6(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 ={v} base_8(D)->ERFIER; _2 = _1 | 4026531840; base_8(D)->ERFIER ={v} _2; goto ; [INV] : # DEBUG BEGIN_STMT _3 ={v} base_8(D)->ERFIER; _4 = _3 & 268435455; base_8(D)->ERFIER ={v} _4; : return; } FlexCAN_IsEnhancedRxFifoEnabled (const struct FLEXCAN_Type * base) { long unsigned int _1; signed int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} base_4(D)->ERFCR; _2 = (signed int) _1; _5 = _2 < 0; return _5; } FlexCAN_SetRxMaskType (struct FLEXCAN_Type * base, Flexcan_Ip_RxMaskType type) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; : # DEBUG BEGIN_STMT if (type_6(D) == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 ={v} base_8(D)->MCR; _2 = _1 & 4294901759; base_8(D)->MCR ={v} _2; goto ; [INV] : # DEBUG BEGIN_STMT _3 ={v} base_8(D)->MCR; _4 = _3 | 65536; base_8(D)->MCR ={v} _4; : return; } FlexCAN_SetTxArbitrationStartDelay (struct FLEXCAN_Type * base, uint8 tasd) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; : # DEBUG BEGIN_STMT _1 ={v} base_8(D)->CTRL2; _2 = _1 & 4278714367; _3 = (long unsigned int) tasd_9(D); _4 = _3 << 19; _5 = _4 & 16252928; _6 = _2 | _5; base_8(D)->CTRL2 ={v} _6; return; } FlexCAN_IsFreezeMode (const struct FLEXCAN_Type * base) { long unsigned int _1; long unsigned int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} base_4(D)->MCR; _2 = _1 & 16777216; _5 = _2 != 0; return _5; } FlexCAN_SetRxIndividualMask (struct FLEXCAN_Type * base, uint32 msgBuffIdx, uint32 mask) { : # DEBUG BEGIN_STMT base_2(D)->RXIMR[msgBuffIdx_3(D)] ={v} mask_4(D); return; } FlexCAN_SetRxMsgBuffGlobalMask (struct FLEXCAN_Type * base, uint32 Mask) { : # DEBUG BEGIN_STMT base_2(D)->RXMGMASK ={v} Mask_3(D); return; } FlexCAN_GetMsgBuffIntStatusFlag (const struct FLEXCAN_Type * base, uint32 msgBuffIdx) { uint32 mask; uint8 flag; long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; unsigned char _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; unsigned char _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; unsigned char _15; uint8 _27; : # DEBUG BEGIN_STMT flag_17 = 0; # DEBUG flag => flag_17 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 31) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT mask_25 ={v} base_20(D)->IMASK1; # DEBUG mask => mask_25 # DEBUG BEGIN_STMT _1 ={v} base_20(D)->IFLAG1; _2 = mask_25 & _1; _3 = msgBuffIdx_18(D) & 31; _4 = _2 >> _3; _5 = (unsigned char) _4; flag_26 = _5 & 1; # DEBUG flag => flag_26 goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 63) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT mask_23 ={v} base_20(D)->IMASK2; # DEBUG mask => mask_23 # DEBUG BEGIN_STMT _6 ={v} base_20(D)->IFLAG2; _7 = mask_23 & _6; _8 = msgBuffIdx_18(D) & 31; _9 = _7 >> _8; _10 = (unsigned char) _9; flag_24 = _10 & 1; # DEBUG flag => flag_24 goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT mask_21 ={v} base_20(D)->IMASK3; # DEBUG mask => mask_21 # DEBUG BEGIN_STMT _11 ={v} base_20(D)->IFLAG3; _12 = mask_21 & _11; _13 = msgBuffIdx_18(D) & 31; _14 = _12 >> _13; _15 = (unsigned char) _14; flag_22 = _15 & 1; # DEBUG flag => flag_22 : # flag_16 = PHI # DEBUG flag => flag_16 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _27 = flag_16; return _27; } RxFifoOcuppiedLastMsgBuff (uint32 x) { long unsigned int _1; long unsigned int _2; long unsigned int _3; uint32 _5; : # DEBUG BEGIN_STMT _1 = x_4(D) + 1; _2 = _1 * 8; _3 = _2 / 4; _5 = _3 + 5; return _5; } FlexCAN_IsListenOnlyModeEnabled (const struct FLEXCAN_Type * base) { long unsigned int _1; long unsigned int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} base_4(D)->CTRL1; _2 = _1 & 8; _5 = _2 != 0; return _5; } FlexCAN_IsFDEnabled (const struct FLEXCAN_Type * base) { long unsigned int _1; long unsigned int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} base_4(D)->MCR; _2 = _1 & 2048; _5 = _2 != 0; return _5; } FlexCAN_SetSelfReception (struct FLEXCAN_Type * base, boolean enable) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int iftmp.3_4; long unsigned int iftmp.3_8; long unsigned int iftmp.3_9; : # DEBUG BEGIN_STMT _1 ={v} base_6(D)->MCR; _2 = _1 & 4294836223; if (enable_7(D) != 0) goto ; [INV] else goto ; [INV] : iftmp.3_9 = 0; goto ; [INV] : iftmp.3_8 = 131072; : # iftmp.3_4 = PHI _3 = iftmp.3_4 | _2; base_6(D)->MCR ={v} _3; return; } FlexCAN_EnhCbtEnable (struct FLEXCAN_Type * base, boolean enableCBT) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int iftmp.6_4; long unsigned int iftmp.6_8; long unsigned int iftmp.6_9; : # DEBUG BEGIN_STMT _1 ={v} base_6(D)->CTRL2; _2 = _1 & 4294959103; if (enableCBT_7(D) != 0) goto ; [INV] else goto ; [INV] : iftmp.6_9 = 8192; goto ; [INV] : iftmp.6_8 = 0; : # iftmp.6_4 = PHI _3 = iftmp.6_4 | _2; base_6(D)->CTRL2 ={v} _3; return; } FlexCAN_EnableExtCbt (struct FLEXCAN_Type * base, boolean enableCBT) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int iftmp.4_4; long unsigned int iftmp.4_8; long unsigned int iftmp.4_9; : # DEBUG BEGIN_STMT _1 ={v} base_6(D)->CBT; _2 = _1 & 2147483647; if (enableCBT_7(D) != 0) goto ; [INV] else goto ; [INV] : iftmp.4_9 = 2147483648; goto ; [INV] : iftmp.4_8 = 0; : # iftmp.4_4 = PHI _3 = iftmp.4_4 | _2; base_6(D)->CBT ={v} _3; return; } FlexCAN_IsEnhCbtEnabled (const struct FLEXCAN_Type * pBase) { long unsigned int _1; long unsigned int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} pBase_4(D)->CTRL2; _2 = _1 & 8192; _5 = _2 != 0; return _5; } FlexCAN_IsExCbtEnabled (const struct FLEXCAN_Type * pBase) { long unsigned int _1; signed int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} pBase_4(D)->CBT; _2 = (signed int) _1; _5 = _2 < 0; return _5; } FlexCAN_GetFDTimeSegments (const struct FLEXCAN_Type * base, struct Flexcan_Ip_TimeSegmentType * timeSeg) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; : # DEBUG BEGIN_STMT _1 ={v} base_16(D)->FDCBT; _2 = _1 >> 20; _3 = _2 & 1023; timeSeg_17(D)->preDivider = _3; # DEBUG BEGIN_STMT _4 ={v} base_16(D)->FDCBT; _5 = _4 >> 10; _6 = _5 & 31; timeSeg_17(D)->propSeg = _6; # DEBUG BEGIN_STMT _7 ={v} base_16(D)->FDCBT; _8 = _7 >> 5; _9 = _8 & 7; timeSeg_17(D)->phaseSeg1 = _9; # DEBUG BEGIN_STMT _10 ={v} base_16(D)->FDCBT; _11 = _10 & 7; timeSeg_17(D)->phaseSeg2 = _11; # DEBUG BEGIN_STMT _12 ={v} base_16(D)->FDCBT; _13 = _12 >> 16; _14 = _13 & 7; timeSeg_17(D)->rJumpwidth = _14; return; } FlexCAN_GetTimeSegments (const struct FLEXCAN_Type * base, struct Flexcan_Ip_TimeSegmentType * timeSeg) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; : # DEBUG BEGIN_STMT _1 ={v} base_16(D)->CTRL1; _2 = _1 >> 24; _3 = _2 & 255; timeSeg_17(D)->preDivider = _3; # DEBUG BEGIN_STMT _4 ={v} base_16(D)->CTRL1; _5 = _4 & 7; timeSeg_17(D)->propSeg = _5; # DEBUG BEGIN_STMT _6 ={v} base_16(D)->CTRL1; _7 = _6 >> 19; _8 = _7 & 7; timeSeg_17(D)->phaseSeg1 = _8; # DEBUG BEGIN_STMT _9 ={v} base_16(D)->CTRL1; _10 = _9 >> 16; _11 = _10 & 7; timeSeg_17(D)->phaseSeg2 = _11; # DEBUG BEGIN_STMT _12 ={v} base_16(D)->CTRL1; _13 = _12 >> 22; _14 = _13 & 3; timeSeg_17(D)->rJumpwidth = _14; return; } FlexCAN_GetExtendedTimeSegments (const struct FLEXCAN_Type * base, struct Flexcan_Ip_TimeSegmentType * timeSeg) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; : # DEBUG BEGIN_STMT _1 ={v} base_16(D)->CBT; _2 = _1 >> 21; _3 = _2 & 1023; timeSeg_17(D)->preDivider = _3; # DEBUG BEGIN_STMT _4 ={v} base_16(D)->CBT; _5 = _4 >> 10; _6 = _5 & 63; timeSeg_17(D)->propSeg = _6; # DEBUG BEGIN_STMT _7 ={v} base_16(D)->CBT; _8 = _7 >> 5; _9 = _8 & 31; timeSeg_17(D)->phaseSeg1 = _9; # DEBUG BEGIN_STMT _10 ={v} base_16(D)->CBT; _11 = _10 & 31; timeSeg_17(D)->phaseSeg2 = _11; # DEBUG BEGIN_STMT _12 ={v} base_16(D)->CBT; _13 = _12 >> 16; _14 = _13 & 31; timeSeg_17(D)->rJumpwidth = _14; return; } FlexCAN_GetEnhancedDataTimeSegments (const struct FLEXCAN_Type * base, struct Flexcan_Ip_TimeSegmentType * timeSeg) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; : # DEBUG BEGIN_STMT _1 = timeSeg_13(D) != 0B; DevAssert (_1); # DEBUG BEGIN_STMT timeSeg_13(D)->propSeg = 0; # DEBUG BEGIN_STMT _2 ={v} base_17(D)->EDCBT; _3 = _2 & 31; timeSeg_13(D)->phaseSeg1 = _3; # DEBUG BEGIN_STMT _4 ={v} base_17(D)->EDCBT; _5 = _4 >> 12; _6 = _5 & 15; timeSeg_13(D)->phaseSeg2 = _6; # DEBUG BEGIN_STMT _7 ={v} base_17(D)->EDCBT; _8 = _7 >> 22; _9 = _8 & 15; timeSeg_13(D)->rJumpwidth = _9; # DEBUG BEGIN_STMT _10 ={v} base_17(D)->EPRS; _11 = _10 >> 16; _12 = _11 & 1023; timeSeg_13(D)->preDivider = _12; return; } FlexCAN_SetEnhancedDataTimeSegments (struct FLEXCAN_Type * base, const struct Flexcan_Ip_TimeSegmentType * timeSeg) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; long unsigned int _16; long unsigned int _17; long unsigned int _18; long unsigned int _19; long unsigned int _20; long unsigned int _21; long unsigned int _22; long unsigned int _23; long unsigned int _24; : # DEBUG BEGIN_STMT _1 = timeSeg_25(D) != 0B; DevAssert (_1); # DEBUG BEGIN_STMT _2 ={v} base_28(D)->EDCBT; _3 = _2 & 4231991264; base_28(D)->EDCBT ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_28(D)->EDCBT; _5 = timeSeg_25(D)->phaseSeg1; _6 = timeSeg_25(D)->propSeg; _7 = _5 + _6; _8 = _7 & 31; _9 = timeSeg_25(D)->phaseSeg2; _10 = _9 << 12; _11 = _10 & 65535; _12 = _8 | _11; _13 = timeSeg_25(D)->rJumpwidth; _14 = _13 << 22; _15 = _14 & 62914560; _16 = _12 | _15; _17 = _4 | _16; base_28(D)->EDCBT ={v} _17; # DEBUG BEGIN_STMT _18 ={v} base_28(D)->EPRS; _19 = _18 & 4227923967; base_28(D)->EPRS ={v} _19; # DEBUG BEGIN_STMT _20 ={v} base_28(D)->EPRS; _21 = timeSeg_25(D)->preDivider; _22 = _21 << 16; _23 = _22 & 67043328; _24 = _20 | _23; base_28(D)->EPRS ={v} _24; return; } FlexCAN_GetEnhancedNominalTimeSegments (const struct FLEXCAN_Type * base, struct Flexcan_Ip_TimeSegmentType * timeSeg) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; : # DEBUG BEGIN_STMT timeSeg_12(D)->propSeg = 0; # DEBUG BEGIN_STMT _1 ={v} base_14(D)->EPRS; _2 = _1 & 1023; timeSeg_12(D)->preDivider = _2; # DEBUG BEGIN_STMT _3 ={v} base_14(D)->ENCBT; _4 = _3 & 255; timeSeg_12(D)->phaseSeg1 = _4; # DEBUG BEGIN_STMT _5 ={v} base_14(D)->ENCBT; _6 = _5 >> 12; _7 = _6 & 127; timeSeg_12(D)->phaseSeg2 = _7; # DEBUG BEGIN_STMT _8 ={v} base_14(D)->ENCBT; _9 = _8 >> 22; _10 = _9 & 127; timeSeg_12(D)->rJumpwidth = _10; return; } FlexCAN_SetEnhancedNominalTimeSegments (struct FLEXCAN_Type * base, const struct Flexcan_Ip_TimeSegmentType * timeSeg) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; long unsigned int _16; long unsigned int _17; long unsigned int _18; long unsigned int _19; long unsigned int _20; long unsigned int _21; long unsigned int _22; long unsigned int _23; long unsigned int _24; : # DEBUG BEGIN_STMT _1 = timeSeg_25(D) != 0B; DevAssert (_1); # DEBUG BEGIN_STMT _2 ={v} base_28(D)->ENCBT; _3 = _2 & 3761770240; base_28(D)->ENCBT ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_28(D)->ENCBT; _5 = timeSeg_25(D)->phaseSeg1; _6 = timeSeg_25(D)->propSeg; _7 = _5 + _6; _8 = _7 + 1; _9 = _8 & 255; _10 = timeSeg_25(D)->phaseSeg2; _11 = _10 << 12; _12 = _11 & 520192; _13 = _9 | _12; _14 = timeSeg_25(D)->rJumpwidth; _15 = _14 << 22; _16 = _15 & 532676608; _17 = _13 | _16; _18 = _4 | _17; base_28(D)->ENCBT ={v} _18; # DEBUG BEGIN_STMT _19 ={v} base_28(D)->EPRS; _20 = _19 & 4294966272; base_28(D)->EPRS ={v} _20; # DEBUG BEGIN_STMT _21 ={v} base_28(D)->EPRS; _22 = timeSeg_25(D)->preDivider; _23 = _22 & 1023; _24 = _21 | _23; base_28(D)->EPRS ={v} _24; return; } FlexCAN_SetExtendedTimeSegments (struct FLEXCAN_Type * base, const struct Flexcan_Ip_TimeSegmentType * timeSeg) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; long unsigned int _16; long unsigned int _17; long unsigned int _18; long unsigned int _19; long unsigned int _20; long unsigned int _21; long unsigned int _22; long unsigned int _23; : # DEBUG BEGIN_STMT _1 = timeSeg_24(D) != 0B; DevAssert (_1); # DEBUG BEGIN_STMT _2 ={v} base_27(D)->CBT; _3 = _2 & 2147483648; base_27(D)->CBT ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_27(D)->CBT; _5 = timeSeg_24(D)->propSeg; _6 = _5 << 10; _7 = _6 & 65535; _8 = timeSeg_24(D)->phaseSeg2; _9 = _8 & 31; _10 = _7 | _9; _11 = timeSeg_24(D)->phaseSeg1; _12 = _11 << 5; _13 = _12 & 992; _14 = _10 | _13; _15 = timeSeg_24(D)->preDivider; _16 = _15 << 21; _17 = _16 & 2145386496; _18 = _14 | _17; _19 = timeSeg_24(D)->rJumpwidth; _20 = _19 << 16; _21 = _20 & 2031616; _22 = _18 | _21; _23 = _4 | _22; base_27(D)->CBT ={v} _23; return; } FlexCAN_SetTimeSegments (struct FLEXCAN_Type * base, const struct Flexcan_Ip_TimeSegmentType * timeSeg) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; long unsigned int _16; long unsigned int _17; long unsigned int _18; long unsigned int _19; long unsigned int _20; long unsigned int _21; long unsigned int _22; : # DEBUG BEGIN_STMT _1 = timeSeg_23(D) != 0B; DevAssert (_1); # DEBUG BEGIN_STMT _2 ={v} base_26(D)->CTRL1; _3 = _2 & 65528; base_26(D)->CTRL1 ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_26(D)->CTRL1; _5 = timeSeg_23(D)->propSeg; _6 = _5 & 7; _7 = timeSeg_23(D)->phaseSeg2; _8 = _7 << 16; _9 = _8 & 458752; _10 = _6 | _9; _11 = timeSeg_23(D)->phaseSeg1; _12 = _11 << 19; _13 = _12 & 3670016; _14 = _10 | _13; _15 = timeSeg_23(D)->preDivider; _16 = _15 << 24; _17 = _14 | _16; _18 = timeSeg_23(D)->rJumpwidth; _19 = _18 << 22; _20 = _19 & 12582912; _21 = _17 | _20; _22 = _4 | _21; base_26(D)->CTRL1 ={v} _22; return; } FlexCAN_SetFDTimeSegments (struct FLEXCAN_Type * base, const struct Flexcan_Ip_TimeSegmentType * timeSeg) { _Bool _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; long unsigned int _16; long unsigned int _17; long unsigned int _18; long unsigned int _19; long unsigned int _20; long unsigned int _21; long unsigned int _22; long unsigned int _23; : # DEBUG BEGIN_STMT _1 = timeSeg_24(D) != 0B; DevAssert (_1); # DEBUG BEGIN_STMT _2 ={v} base_27(D)->FDCBT; _3 = _2 & 3221783320; base_27(D)->FDCBT ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_27(D)->FDCBT; _5 = timeSeg_24(D)->propSeg; _6 = _5 << 10; _7 = _6 & 31744; _8 = timeSeg_24(D)->phaseSeg2; _9 = _8 & 7; _10 = _7 | _9; _11 = timeSeg_24(D)->phaseSeg1; _12 = _11 << 5; _13 = _12 & 255; _14 = _10 | _13; _15 = timeSeg_24(D)->preDivider; _16 = _15 << 20; _17 = _16 & 1072693248; _18 = _14 | _17; _19 = timeSeg_24(D)->rJumpwidth; _20 = _19 << 16; _21 = _20 & 458752; _22 = _18 | _21; _23 = _4 | _22; base_27(D)->FDCBT ={v} _23; return; } FlexCAN_GetBuffStatusImask (const struct FLEXCAN_Type * base, uint32 msgBuffIdx) { uint32 u32Imask; long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; uint8 _24; : # DEBUG BEGIN_STMT u32Imask_17 = 0; # DEBUG u32Imask => u32Imask_17 # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 31) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 ={v} base_20(D)->IMASK1; _2 = msgBuffIdx_18(D) & 31; _3 = 1 << _2; _4 = _1 & _3; _5 = msgBuffIdx_18(D) & 31; u32Imask_23 = _4 >> _5; # DEBUG u32Imask => u32Imask_23 goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 63) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 ={v} base_20(D)->IMASK2; _7 = msgBuffIdx_18(D) & 31; _8 = 1 << _7; _9 = _6 & _8; _10 = msgBuffIdx_18(D) & 31; u32Imask_22 = _9 >> _10; # DEBUG u32Imask => u32Imask_22 goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 ={v} base_20(D)->IMASK3; _12 = msgBuffIdx_18(D) & 31; _13 = 1 << _12; _14 = _11 & _13; _15 = msgBuffIdx_18(D) & 31; u32Imask_21 = _14 >> _15; # DEBUG u32Imask => u32Imask_21 : # u32Imask_16 = PHI # DEBUG u32Imask => u32Imask_16 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _24 = (uint8) u32Imask_16; return _24; } FlexCAN_GetBuffStatusFlag (const struct FLEXCAN_Type * base, uint32 msgBuffIdx) { uint32 flag; long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int _9; long unsigned int _10; long unsigned int _11; long unsigned int _12; long unsigned int _13; long unsigned int _14; long unsigned int _15; uint8 _24; : # DEBUG BEGIN_STMT flag_17 = 0; # DEBUG flag => flag_17 # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 31) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 ={v} base_20(D)->IFLAG1; _2 = msgBuffIdx_18(D) & 31; _3 = 1 << _2; _4 = _1 & _3; _5 = msgBuffIdx_18(D) & 31; flag_23 = _4 >> _5; # DEBUG flag => flag_23 goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 63) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 ={v} base_20(D)->IFLAG2; _7 = msgBuffIdx_18(D) & 31; _8 = 1 << _7; _9 = _6 & _8; _10 = msgBuffIdx_18(D) & 31; flag_22 = _9 >> _10; # DEBUG flag => flag_22 goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_18(D) <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 ={v} base_20(D)->IFLAG3; _12 = msgBuffIdx_18(D) & 31; _13 = 1 << _12; _14 = _11 & _13; _15 = msgBuffIdx_18(D) & 31; flag_21 = _14 >> _15; # DEBUG flag => flag_21 : # flag_16 = PHI # DEBUG flag => flag_16 # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _24 = (uint8) flag_16; return _24; } FlexCAN_ClearMsgBuffIntStatusFlag (struct FLEXCAN_Type * base, uint32 msgBuffIdx) { uint32 flag; long unsigned int _1; : # DEBUG BEGIN_STMT _1 = msgBuffIdx_3(D) & 31; flag_4 = 1 << _1; # DEBUG flag => flag_4 # DEBUG BEGIN_STMT if (msgBuffIdx_3(D) <= 31) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT base_6(D)->IFLAG1 ={v} flag_4; goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_3(D) <= 63) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT base_6(D)->IFLAG2 ={v} flag_4; goto ; [INV] : # DEBUG BEGIN_STMT if (msgBuffIdx_3(D) <= 95) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT base_6(D)->IFLAG3 ={v} flag_4; : # DEBUG BEGIN_STMT return; } FlexCAN_UnlockRxMsgBuff (const struct FLEXCAN_Type * base) { long unsigned int vol.5_3; : # DEBUG BEGIN_STMT vol.5_3 ={v} base_2(D)->TIMER; return; } FlexCAN_SetListenOnlyMode (struct FLEXCAN_Type * base, boolean enableListenOnly) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int iftmp.7_4; long unsigned int iftmp.7_8; long unsigned int iftmp.7_9; : # DEBUG BEGIN_STMT _1 ={v} base_6(D)->CTRL1; _2 = _1 & 4294967287; if (enableListenOnly_7(D) != 0) goto ; [INV] else goto ; [INV] : iftmp.7_9 = 8; goto ; [INV] : iftmp.7_8 = 0; : # iftmp.7_4 = PHI _3 = iftmp.7_4 | _2; base_6(D)->CTRL1 ={v} _3; return; } FlexCAN_SetFDEnabled (struct FLEXCAN_Type * base, boolean enableFD, boolean enableBRS) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; long unsigned int _6; long unsigned int _7; long unsigned int _8; long unsigned int iftmp.1_9; long unsigned int iftmp.2_10; long unsigned int iftmp.1_14; long unsigned int iftmp.1_15; long unsigned int iftmp.2_18; long unsigned int iftmp.2_19; : # DEBUG BEGIN_STMT _1 ={v} base_12(D)->MCR; _2 = _1 & 4294965247; if (enableFD_13(D) != 0) goto ; [INV] else goto ; [INV] : iftmp.1_15 = 2048; goto ; [INV] : iftmp.1_14 = 0; : # iftmp.1_9 = PHI _3 = iftmp.1_9 | _2; base_12(D)->MCR ={v} _3; # DEBUG BEGIN_STMT _4 ={v} base_12(D)->FDCTRL; _5 = _4 & 2147483647; if (enableBRS_17(D) != 0) goto ; [INV] else goto ; [INV] : iftmp.2_19 = 2147483648; goto ; [INV] : iftmp.2_18 = 0; : # iftmp.2_10 = PHI _6 = iftmp.2_10 | _5; base_12(D)->FDCTRL ={v} _6; # DEBUG BEGIN_STMT _7 ={v} base_12(D)->FDCTRL; _8 = _7 & 4294926591; base_12(D)->FDCTRL ={v} _8; return; } FlexCAN_DisableMemErrorDetection (struct FLEXCAN_Type * base) { long unsigned int _1; long unsigned int _2; long unsigned int _3; long unsigned int _4; long unsigned int _5; : # DEBUG BEGIN_STMT _1 ={v} base_7(D)->CTRL2; _2 = _1 | 536870912; base_7(D)->CTRL2 ={v} _2; # DEBUG BEGIN_STMT base_7(D)->MECR ={v} 0; # DEBUG BEGIN_STMT base_7(D)->MECR ={v} 0; # DEBUG BEGIN_STMT _3 ={v} base_7(D)->MECR; _4 = _3 | 256; base_7(D)->MECR ={v} _4; # DEBUG BEGIN_STMT _5 ={v} base_7(D)->CTRL2; base_7(D)->CTRL2 ={v} _5; return; } FlexCAN_IsEnabled (const struct FLEXCAN_Type * pBase) { long unsigned int _1; signed int _2; boolean _5; : # DEBUG BEGIN_STMT _1 ={v} pBase_4(D)->MCR; _2 = (signed int) _1; _5 = _2 >= 0; return _5; } FlexCAN_SetEnhancedTDCOffset (struct FLEXCAN_Type * base, boolean enable, uint8 offset) { uint32 tmp; long unsigned int _1; long unsigned int _2; long unsigned int _3; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT tmp_7 ={v} base_6(D)->ETDC; # DEBUG tmp => tmp_7 # DEBUG BEGIN_STMT tmp_8 = tmp_7 & 2139160575; # DEBUG tmp => tmp_8 # DEBUG BEGIN_STMT if (enable_9(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT tmp_10 = tmp_8 | 2147483648; # DEBUG tmp => tmp_10 # DEBUG BEGIN_STMT _1 = (long unsigned int) offset_11(D); _2 = _1 << 16; _3 = _2 & 8323072; tmp_12 = tmp_10 | _3; # DEBUG tmp => tmp_12 : # tmp_4 = PHI # DEBUG tmp => tmp_4 # DEBUG BEGIN_STMT base_6(D)->ETDC ={v} tmp_4; return; } FlexCAN_SetTDCOffset (struct FLEXCAN_Type * base, boolean enable, uint8 offset) { uint32 tmp; long unsigned int _1; long unsigned int _2; long unsigned int _3; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT tmp_7 ={v} base_6(D)->FDCTRL; # DEBUG tmp => tmp_7 # DEBUG BEGIN_STMT tmp_8 = tmp_7 & 4294926591; # DEBUG tmp => tmp_8 # DEBUG BEGIN_STMT if (enable_9(D) != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT tmp_10 = tmp_8 | 32768; # DEBUG tmp => tmp_10 # DEBUG BEGIN_STMT _1 = (long unsigned int) offset_11(D); _2 = _1 << 8; _3 = _2 & 7936; tmp_12 = tmp_10 | _3; # DEBUG tmp => tmp_12 : # tmp_4 = PHI # DEBUG tmp => tmp_4 # DEBUG BEGIN_STMT base_6(D)->FDCTRL ={v} tmp_4; return; } FlexCAN_SetRxFifoGlobalMask (struct FLEXCAN_Type * base, uint32 Mask) { : # DEBUG BEGIN_STMT base_2(D)->RXFGMASK ={v} Mask_3(D); return; } DevAssert (volatile boolean x) { _Bool x.0_1; : # DEBUG BEGIN_STMT x.0_1 ={v} x; if (x.0_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT return; }