prvAddCurrentTaskToDelayedList (TickType_t xTicksToWait, const BaseType_t xCanBlockIndefinitely) { struct ListItem_t * const pxIndex; const TickType_t xConstTickCount; TickType_t xTimeToWake; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xConstTickCount = xTickCount; # DEBUG BEGIN_STMT pxCurrentTCB.23_1 = pxCurrentTCB; pxCurrentTCB.23_1->ucDelayAborted = 0; # DEBUG BEGIN_STMT pxCurrentTCB.24_2 = pxCurrentTCB; _3 = &pxCurrentTCB.24_2->xStateListItem; _4 = uxListRemove (_3); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTicksToWait == 4294967295) goto ; [INV] else goto ; [INV] : if (xCanBlockIndefinitely != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxIndex = xSuspendedTaskList.pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.25_5 = pxCurrentTCB; pxCurrentTCB.25_5->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT pxCurrentTCB.26_6 = pxCurrentTCB; _7 = pxIndex->pxPrevious; pxCurrentTCB.26_6->xStateListItem.pxPrevious = _7; # DEBUG BEGIN_STMT pxCurrentTCB.27_8 = pxCurrentTCB; _9 = pxIndex->pxPrevious; _10 = &pxCurrentTCB.27_8->xStateListItem; _9->pxNext = _10; # DEBUG BEGIN_STMT pxCurrentTCB.28_11 = pxCurrentTCB; _12 = &pxCurrentTCB.28_11->xStateListItem; pxIndex->pxPrevious = _12; # DEBUG BEGIN_STMT pxCurrentTCB.29_13 = pxCurrentTCB; pxCurrentTCB.29_13->xStateListItem.pvContainer = &xSuspendedTaskList; # DEBUG BEGIN_STMT _14 = xSuspendedTaskList.uxNumberOfItems; _15 = _14 + 1; xSuspendedTaskList.uxNumberOfItems = _15; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT xTimeToWake = xConstTickCount + xTicksToWait; # DEBUG BEGIN_STMT pxCurrentTCB.30_16 = pxCurrentTCB; pxCurrentTCB.30_16->xStateListItem.xItemValue = xTimeToWake; # DEBUG BEGIN_STMT if (xTimeToWake < xConstTickCount) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxOverflowDelayedTaskList.31_17 = pxOverflowDelayedTaskList; pxCurrentTCB.32_18 = pxCurrentTCB; _19 = &pxCurrentTCB.32_18->xStateListItem; vListInsert (pxOverflowDelayedTaskList.31_17, _19); goto ; [INV] : # DEBUG BEGIN_STMT pxDelayedTaskList.33_20 = pxDelayedTaskList; pxCurrentTCB.34_21 = pxCurrentTCB; _22 = &pxCurrentTCB.34_21->xStateListItem; vListInsert (pxDelayedTaskList.33_20, _22); # DEBUG BEGIN_STMT xNextTaskUnblockTime.35_23 = xNextTaskUnblockTime; if (xTimeToWake < xNextTaskUnblockTime.35_23) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xNextTaskUnblockTime = xTimeToWake; : # DEBUG BEGIN_STMT return; } ulTaskGenericNotifyValueClear (struct tskTaskControlBlock * xTask, UBaseType_t uxIndexToClear, uint32_t ulBitsToClear) { uint32_t ulReturn; struct TCB_t * pxTCB; uint32_t D.8233; struct TCB_t * iftmp.164; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.164 = pxCurrentTCB; goto ; [INV] : iftmp.164 = xTask; : pxTCB = iftmp.164; # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT ulReturn = pxTCB->ulNotifiedValue[uxIndexToClear]; # DEBUG BEGIN_STMT _1 = pxTCB->ulNotifiedValue[uxIndexToClear]; _2 = ~ulBitsToClear; _3 = _1 & _2; pxTCB->ulNotifiedValue[uxIndexToClear] = _3; # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.8233 = ulReturn; return D.8233; } xTaskGenericNotifyStateClear (struct tskTaskControlBlock * xTask, UBaseType_t uxIndexToClear) { BaseType_t xReturn; struct TCB_t * pxTCB; BaseType_t D.8227; struct TCB_t * iftmp.163; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxIndexToClear != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.163 = pxCurrentTCB; goto ; [INV] : iftmp.163 = xTask; : pxTCB = iftmp.163; # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT _1 = pxTCB->ucNotifyState[uxIndexToClear]; if (_1 == 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB->ucNotifyState[uxIndexToClear] = 0; # DEBUG BEGIN_STMT xReturn = 1; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; : # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.8227 = xReturn; return D.8227; } vTaskGenericNotifyGiveFromISR (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, BaseType_t * pxHigherPriorityTaskWoken) { struct ListItem_t * const pxIndex; struct ListItem_t * const pxIndex; struct List_t * const pxList; UBaseType_t uxSavedInterruptStatus; uint8_t ucOriginalNotifyState; struct TCB_t * pxTCB; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTaskToNotify == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxIndexToNotify != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortValidateInterruptPriority (); # DEBUG BEGIN_STMT pxTCB = xTaskToNotify; # DEBUG BEGIN_STMT uxSavedInterruptStatus = ulPortRaiseBASEPRI (); # DEBUG BEGIN_STMT ucOriginalNotifyState = pxTCB->ucNotifyState[uxIndexToNotify]; # DEBUG BEGIN_STMT pxTCB->ucNotifyState[uxIndexToNotify] = 2; # DEBUG BEGIN_STMT _1 = pxTCB->ulNotifiedValue[uxIndexToNotify]; _2 = _1 + 1; pxTCB->ulNotifiedValue[uxIndexToNotify] = _2; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (ucOriginalNotifyState == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _3 = pxTCB->xEventListItem.pvContainer; if (_3 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.160_4 = uxSchedulerSuspended; if (uxSchedulerSuspended.160_4 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxList = pxTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _5 = pxTCB->xStateListItem.pxNext; _6 = pxTCB->xStateListItem.pxPrevious; _5->pxPrevious = _6; # DEBUG BEGIN_STMT _7 = pxTCB->xStateListItem.pxPrevious; _8 = pxTCB->xStateListItem.pxNext; _7->pxNext = _8; # DEBUG BEGIN_STMT _9 = pxList->pxIndex; _10 = &pxTCB->xStateListItem; if (_9 == _10) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 = pxTCB->xStateListItem.pxPrevious; pxList->pxIndex = _11; : # DEBUG BEGIN_STMT pxTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _12 = pxList->uxNumberOfItems; _13 = _12 + 4294967295; pxList->uxNumberOfItems = _13; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _14 = pxTCB->uxPriority; uxTopReadyPriority.161_15 = uxTopReadyPriority; if (_14 > uxTopReadyPriority.161_15) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _16 = pxTCB->uxPriority; uxTopReadyPriority = _16; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _17 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_17].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _18 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _18; # DEBUG BEGIN_STMT _19 = pxIndex->pxPrevious; _20 = &pxTCB->xStateListItem; _19->pxNext = _20; # DEBUG BEGIN_STMT _21 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _21; # DEBUG BEGIN_STMT _22 = pxTCB->uxPriority; _23 = &pxReadyTasksLists[_22]; pxTCB->xStateListItem.pvContainer = _23; # DEBUG BEGIN_STMT _24 = pxTCB->uxPriority; _25 = pxReadyTasksLists[_24].uxNumberOfItems; _26 = _25 + 1; pxReadyTasksLists[_24].uxNumberOfItems = _26; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT pxIndex = xPendingReadyList.pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xEventListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _27 = pxIndex->pxPrevious; pxTCB->xEventListItem.pxPrevious = _27; # DEBUG BEGIN_STMT _28 = pxIndex->pxPrevious; _29 = &pxTCB->xEventListItem; _28->pxNext = _29; # DEBUG BEGIN_STMT _30 = &pxTCB->xEventListItem; pxIndex->pxPrevious = _30; # DEBUG BEGIN_STMT pxTCB->xEventListItem.pvContainer = &xPendingReadyList; # DEBUG BEGIN_STMT _31 = xPendingReadyList.uxNumberOfItems; _32 = _31 + 1; xPendingReadyList.uxNumberOfItems = _32; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _33 = pxTCB->uxPriority; pxCurrentTCB.162_34 = pxCurrentTCB; _35 = pxCurrentTCB.162_34->uxPriority; if (_33 > _35) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (pxHigherPriorityTaskWoken != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT *pxHigherPriorityTaskWoken = 1; : # DEBUG BEGIN_STMT xYieldPending = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortSetBASEPRI (uxSavedInterruptStatus); return; } xTaskGenericNotifyFromISR (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t * pulPreviousNotificationValue, BaseType_t * pxHigherPriorityTaskWoken) { struct ListItem_t * const pxIndex; struct ListItem_t * const pxIndex; struct List_t * const pxList; UBaseType_t uxSavedInterruptStatus; BaseType_t xReturn; uint8_t ucOriginalNotifyState; struct TCB_t * pxTCB; BaseType_t D.8195; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xReturn = 1; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTaskToNotify == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxIndexToNotify != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortValidateInterruptPriority (); # DEBUG BEGIN_STMT pxTCB = xTaskToNotify; # DEBUG BEGIN_STMT uxSavedInterruptStatus = ulPortRaiseBASEPRI (); # DEBUG BEGIN_STMT if (pulPreviousNotificationValue != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 = pxTCB->ulNotifiedValue[uxIndexToNotify]; *pulPreviousNotificationValue = _1; : # DEBUG BEGIN_STMT ucOriginalNotifyState = pxTCB->ucNotifyState[uxIndexToNotify]; # DEBUG BEGIN_STMT pxTCB->ucNotifyState[uxIndexToNotify] = 2; # DEBUG BEGIN_STMT switch (eAction) [INV], case 0: [INV], case 1: [INV], case 2: [INV], case 3: [INV], case 4: [INV]> : : # DEBUG BEGIN_STMT _2 = pxTCB->ulNotifiedValue[uxIndexToNotify]; _3 = ulValue | _2; pxTCB->ulNotifiedValue[uxIndexToNotify] = _3; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT _4 = pxTCB->ulNotifiedValue[uxIndexToNotify]; _5 = _4 + 1; pxTCB->ulNotifiedValue[uxIndexToNotify] = _5; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT if (ucOriginalNotifyState != 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; goto ; [INV] : : # DEBUG BEGIN_STMT xTickCount.156_6 = xTickCount; if (xTickCount.156_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (ucOriginalNotifyState == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = pxTCB->xEventListItem.pvContainer; if (_7 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.157_8 = uxSchedulerSuspended; if (uxSchedulerSuspended.157_8 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxList = pxTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _9 = pxTCB->xStateListItem.pxNext; _10 = pxTCB->xStateListItem.pxPrevious; _9->pxPrevious = _10; # DEBUG BEGIN_STMT _11 = pxTCB->xStateListItem.pxPrevious; _12 = pxTCB->xStateListItem.pxNext; _11->pxNext = _12; # DEBUG BEGIN_STMT _13 = pxList->pxIndex; _14 = &pxTCB->xStateListItem; if (_13 == _14) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _15 = pxTCB->xStateListItem.pxPrevious; pxList->pxIndex = _15; : # DEBUG BEGIN_STMT pxTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _16 = pxList->uxNumberOfItems; _17 = _16 + 4294967295; pxList->uxNumberOfItems = _17; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _18 = pxTCB->uxPriority; uxTopReadyPriority.158_19 = uxTopReadyPriority; if (_18 > uxTopReadyPriority.158_19) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _20 = pxTCB->uxPriority; uxTopReadyPriority = _20; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _21 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_21].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _22 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _22; # DEBUG BEGIN_STMT _23 = pxIndex->pxPrevious; _24 = &pxTCB->xStateListItem; _23->pxNext = _24; # DEBUG BEGIN_STMT _25 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _25; # DEBUG BEGIN_STMT _26 = pxTCB->uxPriority; _27 = &pxReadyTasksLists[_26]; pxTCB->xStateListItem.pvContainer = _27; # DEBUG BEGIN_STMT _28 = pxTCB->uxPriority; _29 = pxReadyTasksLists[_28].uxNumberOfItems; _30 = _29 + 1; pxReadyTasksLists[_28].uxNumberOfItems = _30; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT pxIndex = xPendingReadyList.pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xEventListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _31 = pxIndex->pxPrevious; pxTCB->xEventListItem.pxPrevious = _31; # DEBUG BEGIN_STMT _32 = pxIndex->pxPrevious; _33 = &pxTCB->xEventListItem; _32->pxNext = _33; # DEBUG BEGIN_STMT _34 = &pxTCB->xEventListItem; pxIndex->pxPrevious = _34; # DEBUG BEGIN_STMT pxTCB->xEventListItem.pvContainer = &xPendingReadyList; # DEBUG BEGIN_STMT _35 = xPendingReadyList.uxNumberOfItems; _36 = _35 + 1; xPendingReadyList.uxNumberOfItems = _36; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _37 = pxTCB->uxPriority; pxCurrentTCB.159_38 = pxCurrentTCB; _39 = pxCurrentTCB.159_38->uxPriority; if (_37 > _39) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (pxHigherPriorityTaskWoken != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT *pxHigherPriorityTaskWoken = 1; : # DEBUG BEGIN_STMT xYieldPending = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortSetBASEPRI (uxSavedInterruptStatus); # DEBUG BEGIN_STMT D.8195 = xReturn; return D.8195; } xTaskGenericNotify (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t * pulPreviousNotificationValue) { struct ListItem_t * const pxIndex; struct List_t * const pxList; uint8_t ucOriginalNotifyState; BaseType_t xReturn; struct TCB_t * pxTCB; BaseType_t D.8165; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xReturn = 1; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxIndexToNotify != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTaskToNotify == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB = xTaskToNotify; # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT if (pulPreviousNotificationValue != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 = pxTCB->ulNotifiedValue[uxIndexToNotify]; *pulPreviousNotificationValue = _1; : # DEBUG BEGIN_STMT ucOriginalNotifyState = pxTCB->ucNotifyState[uxIndexToNotify]; # DEBUG BEGIN_STMT pxTCB->ucNotifyState[uxIndexToNotify] = 2; # DEBUG BEGIN_STMT switch (eAction) [INV], case 0: [INV], case 1: [INV], case 2: [INV], case 3: [INV], case 4: [INV]> : : # DEBUG BEGIN_STMT _2 = pxTCB->ulNotifiedValue[uxIndexToNotify]; _3 = ulValue | _2; pxTCB->ulNotifiedValue[uxIndexToNotify] = _3; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT _4 = pxTCB->ulNotifiedValue[uxIndexToNotify]; _5 = _4 + 1; pxTCB->ulNotifiedValue[uxIndexToNotify] = _5; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT if (ucOriginalNotifyState != 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; goto ; [INV] : : # DEBUG BEGIN_STMT xTickCount.153_6 = xTickCount; if (xTickCount.153_6 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (ucOriginalNotifyState == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxList = pxTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _7 = pxTCB->xStateListItem.pxNext; _8 = pxTCB->xStateListItem.pxPrevious; _7->pxPrevious = _8; # DEBUG BEGIN_STMT _9 = pxTCB->xStateListItem.pxPrevious; _10 = pxTCB->xStateListItem.pxNext; _9->pxNext = _10; # DEBUG BEGIN_STMT _11 = pxList->pxIndex; _12 = &pxTCB->xStateListItem; if (_11 == _12) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = pxTCB->xStateListItem.pxPrevious; pxList->pxIndex = _13; : # DEBUG BEGIN_STMT pxTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _14 = pxList->uxNumberOfItems; _15 = _14 + 4294967295; pxList->uxNumberOfItems = _15; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _16 = pxTCB->uxPriority; uxTopReadyPriority.154_17 = uxTopReadyPriority; if (_16 > uxTopReadyPriority.154_17) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _18 = pxTCB->uxPriority; uxTopReadyPriority = _18; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _19 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_19].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _20 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _20; # DEBUG BEGIN_STMT _21 = pxIndex->pxPrevious; _22 = &pxTCB->xStateListItem; _21->pxNext = _22; # DEBUG BEGIN_STMT _23 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _23; # DEBUG BEGIN_STMT _24 = pxTCB->uxPriority; _25 = &pxReadyTasksLists[_24]; pxTCB->xStateListItem.pvContainer = _25; # DEBUG BEGIN_STMT _26 = pxTCB->uxPriority; _27 = pxReadyTasksLists[_26].uxNumberOfItems; _28 = _27 + 1; pxReadyTasksLists[_26].uxNumberOfItems = _28; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _29 = pxTCB->xEventListItem.pvContainer; if (_29 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _30 = pxTCB->uxPriority; pxCurrentTCB.155_31 = pxCurrentTCB; _32 = pxCurrentTCB.155_31->uxPriority; if (_30 > _32) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _33 = 3758157060B; *_33 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.8165 = xReturn; return D.8165; } xTaskGenericNotifyWait (UBaseType_t uxIndexToWait, uint32_t ulBitsToClearOnEntry, uint32_t ulBitsToClearOnExit, uint32_t * pulNotificationValue, TickType_t xTicksToWait) { BaseType_t xReturn; BaseType_t D.8140; struct TCB_t * pxCurrentTCB.151; struct TCB_t * pxCurrentTCB.147; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxIndexToWait != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT pxCurrentTCB.146_1 = pxCurrentTCB; _2 = pxCurrentTCB.146_1->ucNotifyState[uxIndexToWait]; if (_2 != 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.147 = pxCurrentTCB; _3 = pxCurrentTCB.147->ulNotifiedValue[uxIndexToWait]; _4 = ~ulBitsToClearOnEntry; _5 = _3 & _4; pxCurrentTCB.147->ulNotifiedValue[uxIndexToWait] = _5; # DEBUG BEGIN_STMT pxCurrentTCB.148_6 = pxCurrentTCB; pxCurrentTCB.148_6->ucNotifyState[uxIndexToWait] = 1; # DEBUG BEGIN_STMT if (xTicksToWait != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT prvAddCurrentTaskToDelayedList (xTicksToWait, 1); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _7 = 3758157060B; *_7 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (pulNotificationValue != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.149_8 = pxCurrentTCB; _9 = pxCurrentTCB.149_8->ulNotifiedValue[uxIndexToWait]; *pulNotificationValue = _9; : # DEBUG BEGIN_STMT pxCurrentTCB.150_10 = pxCurrentTCB; _11 = pxCurrentTCB.150_10->ucNotifyState[uxIndexToWait]; if (_11 != 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.151 = pxCurrentTCB; _12 = pxCurrentTCB.151->ulNotifiedValue[uxIndexToWait]; _13 = ~ulBitsToClearOnExit; _14 = _12 & _13; pxCurrentTCB.151->ulNotifiedValue[uxIndexToWait] = _14; # DEBUG BEGIN_STMT xReturn = 1; : # DEBUG BEGIN_STMT pxCurrentTCB.152_15 = pxCurrentTCB; pxCurrentTCB.152_15->ucNotifyState[uxIndexToWait] = 0; # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.8140 = xReturn; return D.8140; } ulTaskGenericNotifyTake (UBaseType_t uxIndexToWait, BaseType_t xClearCountOnExit, TickType_t xTicksToWait) { uint32_t ulReturn; uint32_t D.8123; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxIndexToWait != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT pxCurrentTCB.140_1 = pxCurrentTCB; _2 = pxCurrentTCB.140_1->ulNotifiedValue[uxIndexToWait]; if (_2 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.141_3 = pxCurrentTCB; pxCurrentTCB.141_3->ucNotifyState[uxIndexToWait] = 1; # DEBUG BEGIN_STMT if (xTicksToWait != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT prvAddCurrentTaskToDelayedList (xTicksToWait, 1); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _4 = 3758157060B; *_4 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.142_5 = pxCurrentTCB; ulReturn = pxCurrentTCB.142_5->ulNotifiedValue[uxIndexToWait]; # DEBUG BEGIN_STMT if (ulReturn != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (xClearCountOnExit != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.143_6 = pxCurrentTCB; pxCurrentTCB.143_6->ulNotifiedValue[uxIndexToWait] = 0; goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.144_7 = pxCurrentTCB; _8 = ulReturn + 4294967295; pxCurrentTCB.144_7->ulNotifiedValue[uxIndexToWait] = _8; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.145_9 = pxCurrentTCB; pxCurrentTCB.145_9->ucNotifyState[uxIndexToWait] = 0; # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.8123 = ulReturn; return D.8123; } pvTaskIncrementMutexHeldCount () { struct tskTaskControlBlock * D.8107; : # DEBUG BEGIN_STMT pxCurrentTCB.138_1 = pxCurrentTCB; if (pxCurrentTCB.138_1 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.139_2 = pxCurrentTCB; _3 = pxCurrentTCB.139_2->uxMutexesHeld; _4 = _3 + 1; pxCurrentTCB.139_2->uxMutexesHeld = _4; : # DEBUG BEGIN_STMT D.8107 = pxCurrentTCB; return D.8107; } uxTaskResetEventItemValue () { TickType_t uxReturn; TickType_t D.8103; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.135_1 = pxCurrentTCB; uxReturn = pxCurrentTCB.135_1->xEventListItem.xItemValue; # DEBUG BEGIN_STMT pxCurrentTCB.136_2 = pxCurrentTCB; _3 = pxCurrentTCB.136_2->uxPriority; pxCurrentTCB.137_4 = pxCurrentTCB; _5 = 5 - _3; pxCurrentTCB.137_4->xEventListItem.xItemValue = _5; # DEBUG BEGIN_STMT D.8103 = uxReturn; return D.8103; } vTaskList (char * pcWriteBuffer) { char cStatus; UBaseType_t x; UBaseType_t uxArraySize; struct TaskStatus_t * pxTaskStatusArray; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT *pcWriteBuffer = 0; # DEBUG BEGIN_STMT uxArraySize = uxCurrentNumberOfTasks; # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.134_1 = uxCurrentNumberOfTasks; _2 = uxCurrentNumberOfTasks.134_1 * 36; pxTaskStatusArray = pvPortMalloc (_2); # DEBUG BEGIN_STMT if (pxTaskStatusArray != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxArraySize = uxTaskGetSystemState (pxTaskStatusArray, uxArraySize, 0B); # DEBUG BEGIN_STMT x = 0; goto ; [INV] : # DEBUG BEGIN_STMT _3 = x * 36; _4 = pxTaskStatusArray + _3; _5 = _4->eCurrentState; switch (_5) [INV], case 0: [INV], case 1: [INV], case 2: [INV], case 3: [INV], case 4: [INV]> : : # DEBUG BEGIN_STMT cStatus = 88; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT cStatus = 82; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT cStatus = 66; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT cStatus = 83; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT cStatus = 68; # DEBUG BEGIN_STMT goto ; [INV] : : # DEBUG BEGIN_STMT cStatus = 0; # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT _6 = x * 36; _7 = pxTaskStatusArray + _6; _8 = _7->pcTaskName; pcWriteBuffer = prvWriteNameToBuffer (pcWriteBuffer, _8); # DEBUG BEGIN_STMT _9 = (int) cStatus; _10 = x * 36; _11 = pxTaskStatusArray + _10; _12 = _11->uxCurrentPriority; _13 = x * 36; _14 = pxTaskStatusArray + _13; _15 = _14->usStackHighWaterMark; _16 = (unsigned int) _15; _17 = x * 36; _18 = pxTaskStatusArray + _17; _19 = _18->xTaskNumber; sprintf (pcWriteBuffer, "\t%c\t%u\t%u\t%u\r\n", _9, _12, _16, _19); # DEBUG BEGIN_STMT _20 = strlen (pcWriteBuffer); pcWriteBuffer = pcWriteBuffer + _20; # DEBUG BEGIN_STMT x = x + 1; : # DEBUG BEGIN_STMT if (x < uxArraySize) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortFree (pxTaskStatusArray); : # DEBUG BEGIN_STMT return; } prvWriteNameToBuffer (char * pcBuffer, const char * pcTaskName) { size_t x; char * D.8101; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT strcpy (pcBuffer, pcTaskName); # DEBUG BEGIN_STMT x = strlen (pcBuffer); goto ; [INV] : # DEBUG BEGIN_STMT _1 = pcBuffer + x; *_1 = 32; # DEBUG BEGIN_STMT x = x + 1; : # DEBUG BEGIN_STMT if (x <= 8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _2 = pcBuffer + x; *_2 = 0; # DEBUG BEGIN_STMT D.8101 = pcBuffer + x; return D.8101; } vTaskPriorityDisinheritAfterTimeout (struct tskTaskControlBlock * const pxMutexHolder, UBaseType_t uxHighestPriorityWaitingTask) { struct ListItem_t * const pxIndex; const UBaseType_t uxOnlyOneMutexHeld; UBaseType_t uxPriorityToUse; UBaseType_t uxPriorityUsedOnEntry; struct TCB_t * const pxTCB; : # DEBUG BEGIN_STMT pxTCB = pxMutexHolder; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxOnlyOneMutexHeld = 1; # DEBUG BEGIN_STMT if (pxMutexHolder != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 = pxTCB->uxMutexesHeld; if (_1 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _2 = pxTCB->uxBasePriority; if (uxHighestPriorityWaitingTask > _2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxPriorityToUse = uxHighestPriorityWaitingTask; goto ; [INV] : # DEBUG BEGIN_STMT uxPriorityToUse = pxTCB->uxBasePriority; : # DEBUG BEGIN_STMT _3 = pxTCB->uxPriority; if (uxPriorityToUse != _3) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = pxTCB->uxMutexesHeld; if (_4 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.132_5 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.132_5) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxPriorityUsedOnEntry = pxTCB->uxPriority; # DEBUG BEGIN_STMT pxTCB->uxPriority = uxPriorityToUse; # DEBUG BEGIN_STMT _6 = pxTCB->xEventListItem.xItemValue; _7 = (signed int) _6; if (_7 >= 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = 5 - uxPriorityToUse; pxTCB->xEventListItem.xItemValue = _8; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _9 = pxTCB->xStateListItem.pvContainer; _10 = &pxReadyTasksLists[uxPriorityUsedOnEntry]; if (_9 == _10) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _11 = &pxTCB->xStateListItem; _12 = uxListRemove (_11); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _13 = pxTCB->uxPriority; uxTopReadyPriority.133_14 = uxTopReadyPriority; if (_13 > uxTopReadyPriority.133_14) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _15 = pxTCB->uxPriority; uxTopReadyPriority = _15; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _16 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_16].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _17 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _17; # DEBUG BEGIN_STMT _18 = pxIndex->pxPrevious; _19 = &pxTCB->xStateListItem; _18->pxNext = _19; # DEBUG BEGIN_STMT _20 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _20; # DEBUG BEGIN_STMT _21 = pxTCB->uxPriority; _22 = &pxReadyTasksLists[_21]; pxTCB->xStateListItem.pvContainer = _22; # DEBUG BEGIN_STMT _23 = pxTCB->uxPriority; _24 = pxReadyTasksLists[_23].uxNumberOfItems; _25 = _24 + 1; pxReadyTasksLists[_23].uxNumberOfItems = _25; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT return; } xTaskPriorityDisinherit (struct tskTaskControlBlock * const pxMutexHolder) { struct ListItem_t * const pxIndex; BaseType_t xReturn; struct TCB_t * const pxTCB; BaseType_t D.8069; : # DEBUG BEGIN_STMT pxTCB = pxMutexHolder; # DEBUG BEGIN_STMT xReturn = 0; # DEBUG BEGIN_STMT if (pxMutexHolder != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.130_1 = pxCurrentTCB; if (pxTCB != pxCurrentTCB.130_1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _2 = pxTCB->uxMutexesHeld; if (_2 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _3 = pxTCB->uxMutexesHeld; _4 = _3 + 4294967295; pxTCB->uxMutexesHeld = _4; # DEBUG BEGIN_STMT _5 = pxTCB->uxPriority; _6 = pxTCB->uxBasePriority; if (_5 != _6) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = pxTCB->uxMutexesHeld; if (_7 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = &pxTCB->xStateListItem; _9 = uxListRemove (_8); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _10 = pxTCB->uxBasePriority; pxTCB->uxPriority = _10; # DEBUG BEGIN_STMT _11 = pxTCB->uxPriority; _12 = 5 - _11; pxTCB->xEventListItem.xItemValue = _12; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _13 = pxTCB->uxPriority; uxTopReadyPriority.131_14 = uxTopReadyPriority; if (_13 > uxTopReadyPriority.131_14) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _15 = pxTCB->uxPriority; uxTopReadyPriority = _15; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _16 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_16].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _17 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _17; # DEBUG BEGIN_STMT _18 = pxIndex->pxPrevious; _19 = &pxTCB->xStateListItem; _18->pxNext = _19; # DEBUG BEGIN_STMT _20 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _20; # DEBUG BEGIN_STMT _21 = pxTCB->uxPriority; _22 = &pxReadyTasksLists[_21]; pxTCB->xStateListItem.pvContainer = _22; # DEBUG BEGIN_STMT _23 = pxTCB->uxPriority; _24 = pxReadyTasksLists[_23].uxNumberOfItems; _25 = _24 + 1; pxReadyTasksLists[_23].uxNumberOfItems = _25; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xReturn = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.8069 = xReturn; return D.8069; } xTaskPriorityInherit (struct tskTaskControlBlock * const pxMutexHolder) { struct ListItem_t * const pxIndex; BaseType_t xReturn; struct TCB_t * const pxMutexHolderTCB; BaseType_t D.8049; : # DEBUG BEGIN_STMT pxMutexHolderTCB = pxMutexHolder; # DEBUG BEGIN_STMT xReturn = 0; # DEBUG BEGIN_STMT if (pxMutexHolder != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _1 = pxMutexHolderTCB->uxPriority; pxCurrentTCB.124_2 = pxCurrentTCB; _3 = pxCurrentTCB.124_2->uxPriority; if (_1 < _3) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = pxMutexHolderTCB->xEventListItem.xItemValue; _5 = (signed int) _4; if (_5 >= 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.125_6 = pxCurrentTCB; _7 = pxCurrentTCB.125_6->uxPriority; _8 = 5 - _7; pxMutexHolderTCB->xEventListItem.xItemValue = _8; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _9 = pxMutexHolderTCB->xStateListItem.pvContainer; _10 = pxMutexHolderTCB->uxPriority; _11 = &pxReadyTasksLists[_10]; if (_9 == _11) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _12 = &pxMutexHolderTCB->xStateListItem; _13 = uxListRemove (_12); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.126_14 = pxCurrentTCB; _15 = pxCurrentTCB.126_14->uxPriority; pxMutexHolderTCB->uxPriority = _15; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _16 = pxMutexHolderTCB->uxPriority; uxTopReadyPriority.127_17 = uxTopReadyPriority; if (_16 > uxTopReadyPriority.127_17) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _18 = pxMutexHolderTCB->uxPriority; uxTopReadyPriority = _18; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _19 = pxMutexHolderTCB->uxPriority; pxIndex = pxReadyTasksLists[_19].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxMutexHolderTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _20 = pxIndex->pxPrevious; pxMutexHolderTCB->xStateListItem.pxPrevious = _20; # DEBUG BEGIN_STMT _21 = pxIndex->pxPrevious; _22 = &pxMutexHolderTCB->xStateListItem; _21->pxNext = _22; # DEBUG BEGIN_STMT _23 = &pxMutexHolderTCB->xStateListItem; pxIndex->pxPrevious = _23; # DEBUG BEGIN_STMT _24 = pxMutexHolderTCB->uxPriority; _25 = &pxReadyTasksLists[_24]; pxMutexHolderTCB->xStateListItem.pvContainer = _25; # DEBUG BEGIN_STMT _26 = pxMutexHolderTCB->uxPriority; _27 = pxReadyTasksLists[_26].uxNumberOfItems; _28 = _27 + 1; pxReadyTasksLists[_26].uxNumberOfItems = _28; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.128_29 = pxCurrentTCB; _30 = pxCurrentTCB.128_29->uxPriority; pxMutexHolderTCB->uxPriority = _30; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xReturn = 1; goto ; [INV] : # DEBUG BEGIN_STMT _31 = pxMutexHolderTCB->uxBasePriority; pxCurrentTCB.129_32 = pxCurrentTCB; _33 = pxCurrentTCB.129_32->uxPriority; if (_31 < _33) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.8049 = xReturn; return D.8049; } xTaskGetSchedulerState () { BaseType_t xReturn; BaseType_t D.8027; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xSchedulerRunning.122_1 = xSchedulerRunning; if (xSchedulerRunning.122_1 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 1; goto ; [INV] : # DEBUG BEGIN_STMT uxSchedulerSuspended.123_2 = uxSchedulerSuspended; if (uxSchedulerSuspended.123_2 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 2; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; : # DEBUG BEGIN_STMT D.8027 = xReturn; return D.8027; } xTaskGetCurrentTaskHandle () { struct tskTaskControlBlock * xReturn; struct tskTaskControlBlock * D.8019; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xReturn = pxCurrentTCB; # DEBUG BEGIN_STMT D.8019 = xReturn; return D.8019; } prvResetNextTaskUnblockTime () { : # DEBUG BEGIN_STMT pxDelayedTaskList.20_1 = pxDelayedTaskList; _2 = pxDelayedTaskList.20_1->uxNumberOfItems; if (_2 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xNextTaskUnblockTime = 4294967295; goto ; [INV] : # DEBUG BEGIN_STMT pxDelayedTaskList.21_3 = pxDelayedTaskList; _4 = pxDelayedTaskList.21_3->xListEnd.pxNext; _5 = _4->xItemValue; xNextTaskUnblockTime = _5; : return; } prvDeleteTCB (struct TCB_t * pxTCB) { : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = pxTCB->pxStack; vPortFree (_1); # DEBUG BEGIN_STMT vPortFree (pxTCB); return; } uxTaskGetStackHighWaterMark (struct tskTaskControlBlock * xTask) { UBaseType_t uxReturn; uint8_t * pucEndOfStack; struct TCB_t * pxTCB; UBaseType_t D.8017; struct TCB_t * iftmp.121; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.121 = pxCurrentTCB; goto ; [INV] : iftmp.121 = xTask; : pxTCB = iftmp.121; # DEBUG BEGIN_STMT pucEndOfStack = pxTCB->pxStack; # DEBUG BEGIN_STMT _1 = prvTaskCheckFreeStackSpace (pucEndOfStack); uxReturn = (UBaseType_t) _1; # DEBUG BEGIN_STMT D.8017 = uxReturn; return D.8017; } prvTaskCheckFreeStackSpace (const uint8_t * pucStackByte) { uint32_t ulCount; uint16_t D.8011; : # DEBUG BEGIN_STMT ulCount = 0; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT pucStackByte = pucStackByte + 1; # DEBUG BEGIN_STMT ulCount = ulCount + 1; : # DEBUG BEGIN_STMT _1 = *pucStackByte; if (_1 == 165) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT ulCount = ulCount / 4; # DEBUG BEGIN_STMT D.8011 = (uint16_t) ulCount; return D.8011; } prvListTasksWithinSingleList (struct TaskStatus_t * pxTaskStatusArray, struct List_t * pxList, eTaskState eState) { struct List_t * const pxConstList; struct List_t * const pxConstList; UBaseType_t uxTask; struct TCB_t * pxFirstTCB; struct TCB_t * pxNextTCB; UBaseType_t D.7866; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxTask = 0; # DEBUG BEGIN_STMT _1 = pxList->uxNumberOfItems; if (_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxConstList = pxList; # DEBUG BEGIN_STMT _2 = pxConstList->pxIndex; _3 = _2->pxNext; pxConstList->pxIndex = _3; # DEBUG BEGIN_STMT _4 = pxConstList->pxIndex; _5 = &pxConstList->xListEnd; if (_4 == _5) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = pxConstList->pxIndex; _7 = _6->pxNext; pxConstList->pxIndex = _7; : # DEBUG BEGIN_STMT _8 = pxConstList->pxIndex; pxFirstTCB = _8->pvOwner; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxConstList = pxList; # DEBUG BEGIN_STMT _9 = pxConstList->pxIndex; _10 = _9->pxNext; pxConstList->pxIndex = _10; # DEBUG BEGIN_STMT _11 = pxConstList->pxIndex; _12 = &pxConstList->xListEnd; if (_11 == _12) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = pxConstList->pxIndex; _14 = _13->pxNext; pxConstList->pxIndex = _14; : # DEBUG BEGIN_STMT _15 = pxConstList->pxIndex; pxNextTCB = _15->pvOwner; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _16 = uxTask * 36; _17 = pxTaskStatusArray + _16; vTaskGetInfo (pxNextTCB, _17, 1, eState); # DEBUG BEGIN_STMT uxTask = uxTask + 1; # DEBUG BEGIN_STMT if (pxNextTCB != pxFirstTCB) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7866 = uxTask; return D.7866; } vTaskGetInfo (struct tskTaskControlBlock * xTask, struct TaskStatus_t * pxTaskStatus, BaseType_t xGetFreeStackSpace, eTaskState eState) { struct TCB_t * pxTCB; struct TCB_t * iftmp.119; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.119 = pxCurrentTCB; goto ; [INV] : iftmp.119 = xTask; : pxTCB = iftmp.119; # DEBUG BEGIN_STMT pxTaskStatus->xHandle = pxTCB; # DEBUG BEGIN_STMT _1 = &pxTCB->pcTaskName[0]; pxTaskStatus->pcTaskName = _1; # DEBUG BEGIN_STMT _2 = pxTCB->uxPriority; pxTaskStatus->uxCurrentPriority = _2; # DEBUG BEGIN_STMT _3 = pxTCB->pxStack; pxTaskStatus->pxStackBase = _3; # DEBUG BEGIN_STMT _4 = pxTCB->uxTCBNumber; pxTaskStatus->xTaskNumber = _4; # DEBUG BEGIN_STMT _5 = pxTCB->uxBasePriority; pxTaskStatus->uxBasePriority = _5; # DEBUG BEGIN_STMT pxTaskStatus->ulRunTimeCounter = 0; # DEBUG BEGIN_STMT if (eState != 5) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.120_6 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.120_6) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTaskStatus->eCurrentState = 0; goto ; [INV] : # DEBUG BEGIN_STMT pxTaskStatus->eCurrentState = eState; # DEBUG BEGIN_STMT if (eState == 3) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vTaskSuspendAll (); # DEBUG BEGIN_STMT _7 = pxTCB->xEventListItem.pvContainer; if (_7 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTaskStatus->eCurrentState = 2; : # DEBUG BEGIN_STMT xTaskResumeAll (); goto ; [INV] : # DEBUG BEGIN_STMT _8 = eTaskGetState (pxTCB); pxTaskStatus->eCurrentState = _8; : # DEBUG BEGIN_STMT if (xGetFreeStackSpace != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = pxTCB->pxStack; _10 = prvTaskCheckFreeStackSpace (_9); pxTaskStatus->usStackHighWaterMark = _10; goto ; [INV] : # DEBUG BEGIN_STMT pxTaskStatus->usStackHighWaterMark = 0; : return; } prvCheckTasksWaitingTermination () { struct TCB_t * pxTCB; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT _1 = xTasksWaitingTermination.xListEnd.pxNext; pxTCB = _1->pvOwner; # DEBUG BEGIN_STMT _2 = &pxTCB->xStateListItem; uxListRemove (_2); # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.58_3 = uxCurrentNumberOfTasks; _4 = uxCurrentNumberOfTasks.58_3 + 4294967295; uxCurrentNumberOfTasks = _4; # DEBUG BEGIN_STMT uxDeletedTasksWaitingCleanUp.59_5 = uxDeletedTasksWaitingCleanUp; _6 = uxDeletedTasksWaitingCleanUp.59_5 + 4294967295; uxDeletedTasksWaitingCleanUp = _6; # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT prvDeleteTCB (pxTCB); : # DEBUG BEGIN_STMT uxDeletedTasksWaitingCleanUp.60_7 = uxDeletedTasksWaitingCleanUp; if (uxDeletedTasksWaitingCleanUp.60_7 != 0) goto ; [INV] else goto ; [INV] : return; } prvInitialiseTaskLists () { UBaseType_t uxPriority; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxPriority = 0; goto ; [INV] : # DEBUG BEGIN_STMT _1 = &pxReadyTasksLists[uxPriority]; vListInitialise (_1); # DEBUG BEGIN_STMT uxPriority = uxPriority + 1; : # DEBUG BEGIN_STMT if (uxPriority <= 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vListInitialise (&xDelayedTaskList1); # DEBUG BEGIN_STMT vListInitialise (&xDelayedTaskList2); # DEBUG BEGIN_STMT vListInitialise (&xPendingReadyList); # DEBUG BEGIN_STMT vListInitialise (&xTasksWaitingTermination); # DEBUG BEGIN_STMT vListInitialise (&xSuspendedTaskList); # DEBUG BEGIN_STMT pxDelayedTaskList = &xDelayedTaskList1; # DEBUG BEGIN_STMT pxOverflowDelayedTaskList = &xDelayedTaskList2; return; } prvIdleTask (void * pvParameters) { : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT prvCheckTasksWaitingTermination (); # DEBUG BEGIN_STMT _1 = pxReadyTasksLists[0].uxNumberOfItems; if (_1 > 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _2 = 3758157060B; *_2 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT goto ; [INV] } vTaskSetTaskNumber (struct tskTaskControlBlock * xTask, const UBaseType_t uxHandle) { struct TCB_t * pxTCB; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTask != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB = xTask; # DEBUG BEGIN_STMT pxTCB->uxTaskNumber = uxHandle; : return; } uxTaskGetTaskNumber (struct tskTaskControlBlock * xTask) { const struct TCB_t * pxTCB; UBaseType_t uxReturn; UBaseType_t D.7990; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTask != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB = xTask; # DEBUG BEGIN_STMT uxReturn = pxTCB->uxTaskNumber; goto ; [INV] : # DEBUG BEGIN_STMT uxReturn = 0; : # DEBUG BEGIN_STMT D.7990 = uxReturn; return D.7990; } vTaskMissedYield () { : # DEBUG BEGIN_STMT xYieldPending = 1; return; } xTaskCheckForTimeOut (struct TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait) { const TickType_t xElapsedTime; const TickType_t xConstTickCount; BaseType_t xReturn; BaseType_t D.7985; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (pxTimeOut == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (pxTicksToWait == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT xConstTickCount = xTickCount; # DEBUG BEGIN_STMT _1 = pxTimeOut->xTimeOnEntering; xElapsedTime = xConstTickCount - _1; # DEBUG BEGIN_STMT pxCurrentTCB.116_2 = pxCurrentTCB; _3 = pxCurrentTCB.116_2->ucDelayAborted; if (_3 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.117_4 = pxCurrentTCB; pxCurrentTCB.117_4->ucDelayAborted = 0; # DEBUG BEGIN_STMT xReturn = 1; goto ; [INV] : # DEBUG BEGIN_STMT _5 = *pxTicksToWait; if (_5 == 4294967295) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; goto ; [INV] : # DEBUG BEGIN_STMT _6 = pxTimeOut->xOverflowCount; xNumOfOverflows.118_7 = xNumOfOverflows; if (_6 != xNumOfOverflows.118_7) goto ; [INV] else goto ; [INV] : _8 = pxTimeOut->xTimeOnEntering; if (xConstTickCount >= _8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 1; # DEBUG BEGIN_STMT *pxTicksToWait = 0; goto ; [INV] : # DEBUG BEGIN_STMT _9 = *pxTicksToWait; if (xElapsedTime < _9) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _10 = *pxTicksToWait; _11 = _10 - xElapsedTime; *pxTicksToWait = _11; # DEBUG BEGIN_STMT vTaskInternalSetTimeOutState (pxTimeOut); # DEBUG BEGIN_STMT xReturn = 0; goto ; [INV] : # DEBUG BEGIN_STMT *pxTicksToWait = 0; # DEBUG BEGIN_STMT xReturn = 1; : # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.7985 = xReturn; return D.7985; } vTaskInternalSetTimeOutState (struct TimeOut_t * const pxTimeOut) { : # DEBUG BEGIN_STMT xNumOfOverflows.114_1 = xNumOfOverflows; pxTimeOut->xOverflowCount = xNumOfOverflows.114_1; # DEBUG BEGIN_STMT xTickCount.115_2 = xTickCount; pxTimeOut->xTimeOnEntering = xTickCount.115_2; return; } vTaskSetTimeOutState (struct TimeOut_t * const pxTimeOut) { : # DEBUG BEGIN_STMT if (pxTimeOut == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT xNumOfOverflows.112_1 = xNumOfOverflows; pxTimeOut->xOverflowCount = xNumOfOverflows.112_1; # DEBUG BEGIN_STMT xTickCount.113_2 = xTickCount; pxTimeOut->xTimeOnEntering = xTickCount.113_2; # DEBUG BEGIN_STMT vPortExitCritical (); return; } vTaskRemoveFromUnorderedEventList (struct ListItem_t * pxEventListItem, const TickType_t xItemValue) { struct ListItem_t * const pxIndex; struct List_t * const pxList; struct List_t * const pxList; struct TCB_t * pxUnblockedTCB; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.109_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.109_1 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _2 = xItemValue | 2147483648; pxEventListItem->xItemValue = _2; # DEBUG BEGIN_STMT pxUnblockedTCB = pxEventListItem->pvOwner; # DEBUG BEGIN_STMT if (pxUnblockedTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxList = pxEventListItem->pvContainer; # DEBUG BEGIN_STMT _3 = pxEventListItem->pxNext; _4 = pxEventListItem->pxPrevious; _3->pxPrevious = _4; # DEBUG BEGIN_STMT _5 = pxEventListItem->pxPrevious; _6 = pxEventListItem->pxNext; _5->pxNext = _6; # DEBUG BEGIN_STMT _7 = pxList->pxIndex; if (pxEventListItem == _7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = pxEventListItem->pxPrevious; pxList->pxIndex = _8; : # DEBUG BEGIN_STMT pxEventListItem->pvContainer = 0B; # DEBUG BEGIN_STMT _9 = pxList->uxNumberOfItems; _10 = _9 + 4294967295; pxList->uxNumberOfItems = _10; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxList = pxUnblockedTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _11 = pxUnblockedTCB->xStateListItem.pxNext; _12 = pxUnblockedTCB->xStateListItem.pxPrevious; _11->pxPrevious = _12; # DEBUG BEGIN_STMT _13 = pxUnblockedTCB->xStateListItem.pxPrevious; _14 = pxUnblockedTCB->xStateListItem.pxNext; _13->pxNext = _14; # DEBUG BEGIN_STMT _15 = pxList->pxIndex; _16 = &pxUnblockedTCB->xStateListItem; if (_15 == _16) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _17 = pxUnblockedTCB->xStateListItem.pxPrevious; pxList->pxIndex = _17; : # DEBUG BEGIN_STMT pxUnblockedTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _18 = pxList->uxNumberOfItems; _19 = _18 + 4294967295; pxList->uxNumberOfItems = _19; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _20 = pxUnblockedTCB->uxPriority; uxTopReadyPriority.110_21 = uxTopReadyPriority; if (_20 > uxTopReadyPriority.110_21) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _22 = pxUnblockedTCB->uxPriority; uxTopReadyPriority = _22; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _23 = pxUnblockedTCB->uxPriority; pxIndex = pxReadyTasksLists[_23].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxUnblockedTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _24 = pxIndex->pxPrevious; pxUnblockedTCB->xStateListItem.pxPrevious = _24; # DEBUG BEGIN_STMT _25 = pxIndex->pxPrevious; _26 = &pxUnblockedTCB->xStateListItem; _25->pxNext = _26; # DEBUG BEGIN_STMT _27 = &pxUnblockedTCB->xStateListItem; pxIndex->pxPrevious = _27; # DEBUG BEGIN_STMT _28 = pxUnblockedTCB->uxPriority; _29 = &pxReadyTasksLists[_28]; pxUnblockedTCB->xStateListItem.pvContainer = _29; # DEBUG BEGIN_STMT _30 = pxUnblockedTCB->uxPriority; _31 = pxReadyTasksLists[_30].uxNumberOfItems; _32 = _31 + 1; pxReadyTasksLists[_30].uxNumberOfItems = _32; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _33 = pxUnblockedTCB->uxPriority; pxCurrentTCB.111_34 = pxCurrentTCB; _35 = pxCurrentTCB.111_34->uxPriority; if (_33 > _35) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldPending = 1; : return; } xTaskRemoveFromEventList (const struct List_t * const pxEventList) { struct ListItem_t * const pxIndex; struct ListItem_t * const pxIndex; struct List_t * const pxList; struct List_t * const pxList; BaseType_t xReturn; struct TCB_t * pxUnblockedTCB; BaseType_t D.7952; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = pxEventList->xListEnd.pxNext; pxUnblockedTCB = _1->pvOwner; # DEBUG BEGIN_STMT if (pxUnblockedTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxList = pxUnblockedTCB->xEventListItem.pvContainer; # DEBUG BEGIN_STMT _2 = pxUnblockedTCB->xEventListItem.pxNext; _3 = pxUnblockedTCB->xEventListItem.pxPrevious; _2->pxPrevious = _3; # DEBUG BEGIN_STMT _4 = pxUnblockedTCB->xEventListItem.pxPrevious; _5 = pxUnblockedTCB->xEventListItem.pxNext; _4->pxNext = _5; # DEBUG BEGIN_STMT _6 = pxList->pxIndex; _7 = &pxUnblockedTCB->xEventListItem; if (_6 == _7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = pxUnblockedTCB->xEventListItem.pxPrevious; pxList->pxIndex = _8; : # DEBUG BEGIN_STMT pxUnblockedTCB->xEventListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _9 = pxList->uxNumberOfItems; _10 = _9 + 4294967295; pxList->uxNumberOfItems = _10; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.106_11 = uxSchedulerSuspended; if (uxSchedulerSuspended.106_11 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxList = pxUnblockedTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _12 = pxUnblockedTCB->xStateListItem.pxNext; _13 = pxUnblockedTCB->xStateListItem.pxPrevious; _12->pxPrevious = _13; # DEBUG BEGIN_STMT _14 = pxUnblockedTCB->xStateListItem.pxPrevious; _15 = pxUnblockedTCB->xStateListItem.pxNext; _14->pxNext = _15; # DEBUG BEGIN_STMT _16 = pxList->pxIndex; _17 = &pxUnblockedTCB->xStateListItem; if (_16 == _17) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _18 = pxUnblockedTCB->xStateListItem.pxPrevious; pxList->pxIndex = _18; : # DEBUG BEGIN_STMT pxUnblockedTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _19 = pxList->uxNumberOfItems; _20 = _19 + 4294967295; pxList->uxNumberOfItems = _20; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _21 = pxUnblockedTCB->uxPriority; uxTopReadyPriority.107_22 = uxTopReadyPriority; if (_21 > uxTopReadyPriority.107_22) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _23 = pxUnblockedTCB->uxPriority; uxTopReadyPriority = _23; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _24 = pxUnblockedTCB->uxPriority; pxIndex = pxReadyTasksLists[_24].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxUnblockedTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _25 = pxIndex->pxPrevious; pxUnblockedTCB->xStateListItem.pxPrevious = _25; # DEBUG BEGIN_STMT _26 = pxIndex->pxPrevious; _27 = &pxUnblockedTCB->xStateListItem; _26->pxNext = _27; # DEBUG BEGIN_STMT _28 = &pxUnblockedTCB->xStateListItem; pxIndex->pxPrevious = _28; # DEBUG BEGIN_STMT _29 = pxUnblockedTCB->uxPriority; _30 = &pxReadyTasksLists[_29]; pxUnblockedTCB->xStateListItem.pvContainer = _30; # DEBUG BEGIN_STMT _31 = pxUnblockedTCB->uxPriority; _32 = pxReadyTasksLists[_31].uxNumberOfItems; _33 = _32 + 1; pxReadyTasksLists[_31].uxNumberOfItems = _33; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT pxIndex = xPendingReadyList.pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxUnblockedTCB->xEventListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _34 = pxIndex->pxPrevious; pxUnblockedTCB->xEventListItem.pxPrevious = _34; # DEBUG BEGIN_STMT _35 = pxIndex->pxPrevious; _36 = &pxUnblockedTCB->xEventListItem; _35->pxNext = _36; # DEBUG BEGIN_STMT _37 = &pxUnblockedTCB->xEventListItem; pxIndex->pxPrevious = _37; # DEBUG BEGIN_STMT pxUnblockedTCB->xEventListItem.pvContainer = &xPendingReadyList; # DEBUG BEGIN_STMT _38 = xPendingReadyList.uxNumberOfItems; _39 = _38 + 1; xPendingReadyList.uxNumberOfItems = _39; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _40 = pxUnblockedTCB->uxPriority; pxCurrentTCB.108_41 = pxCurrentTCB; _42 = pxCurrentTCB.108_41->uxPriority; if (_40 > _42) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 1; # DEBUG BEGIN_STMT xYieldPending = 1; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; : # DEBUG BEGIN_STMT D.7952 = xReturn; return D.7952; } vTaskPlaceOnEventListRestricted (struct List_t * const pxEventList, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely) { struct ListItem_t * const pxIndex; : # DEBUG BEGIN_STMT if (pxEventList == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxIndex = pxEventList->pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.101_1 = pxCurrentTCB; pxCurrentTCB.101_1->xEventListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT pxCurrentTCB.102_2 = pxCurrentTCB; _3 = pxIndex->pxPrevious; pxCurrentTCB.102_2->xEventListItem.pxPrevious = _3; # DEBUG BEGIN_STMT pxCurrentTCB.103_4 = pxCurrentTCB; _5 = pxIndex->pxPrevious; _6 = &pxCurrentTCB.103_4->xEventListItem; _5->pxNext = _6; # DEBUG BEGIN_STMT pxCurrentTCB.104_7 = pxCurrentTCB; _8 = &pxCurrentTCB.104_7->xEventListItem; pxIndex->pxPrevious = _8; # DEBUG BEGIN_STMT pxCurrentTCB.105_9 = pxCurrentTCB; pxCurrentTCB.105_9->xEventListItem.pvContainer = pxEventList; # DEBUG BEGIN_STMT _10 = pxEventList->uxNumberOfItems; _11 = _10 + 1; pxEventList->uxNumberOfItems = _11; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xWaitIndefinitely != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xTicksToWait = 4294967295; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT prvAddCurrentTaskToDelayedList (xTicksToWait, xWaitIndefinitely); return; } vTaskPlaceOnUnorderedEventList (struct List_t * pxEventList, const TickType_t xItemValue, const TickType_t xTicksToWait) { struct ListItem_t * const pxIndex; : # DEBUG BEGIN_STMT if (pxEventList == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.94_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.94_1 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.95_2 = pxCurrentTCB; _3 = xItemValue | 2147483648; pxCurrentTCB.95_2->xEventListItem.xItemValue = _3; # DEBUG BEGIN_STMT pxIndex = pxEventList->pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.96_4 = pxCurrentTCB; pxCurrentTCB.96_4->xEventListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT pxCurrentTCB.97_5 = pxCurrentTCB; _6 = pxIndex->pxPrevious; pxCurrentTCB.97_5->xEventListItem.pxPrevious = _6; # DEBUG BEGIN_STMT pxCurrentTCB.98_7 = pxCurrentTCB; _8 = pxIndex->pxPrevious; _9 = &pxCurrentTCB.98_7->xEventListItem; _8->pxNext = _9; # DEBUG BEGIN_STMT pxCurrentTCB.99_10 = pxCurrentTCB; _11 = &pxCurrentTCB.99_10->xEventListItem; pxIndex->pxPrevious = _11; # DEBUG BEGIN_STMT pxCurrentTCB.100_12 = pxCurrentTCB; pxCurrentTCB.100_12->xEventListItem.pvContainer = pxEventList; # DEBUG BEGIN_STMT _13 = pxEventList->uxNumberOfItems; _14 = _13 + 1; pxEventList->uxNumberOfItems = _14; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT prvAddCurrentTaskToDelayedList (xTicksToWait, 1); return; } vTaskPlaceOnEventList (struct List_t * const pxEventList, const TickType_t xTicksToWait) { : # DEBUG BEGIN_STMT if (pxEventList == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.93_1 = pxCurrentTCB; _2 = &pxCurrentTCB.93_1->xEventListItem; vListInsert (pxEventList, _2); # DEBUG BEGIN_STMT prvAddCurrentTaskToDelayedList (xTicksToWait, 1); return; } __attribute__((used)) vTaskSwitchContext () { struct List_t * const pxConstList; UBaseType_t uxTopPriority; : # DEBUG BEGIN_STMT uxSchedulerSuspended.92_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.92_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldPending = 1; goto ; [INV] : # DEBUG BEGIN_STMT xYieldPending = 0; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxTopPriority = uxTopReadyPriority; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT if (uxTopPriority == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxTopPriority = uxTopPriority + 4294967295; : # DEBUG BEGIN_STMT _2 = pxReadyTasksLists[uxTopPriority].uxNumberOfItems; if (_2 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxConstList = &pxReadyTasksLists[uxTopPriority]; # DEBUG BEGIN_STMT _3 = pxConstList->pxIndex; _4 = _3->pxNext; pxConstList->pxIndex = _4; # DEBUG BEGIN_STMT _5 = pxConstList->pxIndex; _6 = &pxConstList->xListEnd; if (_5 == _6) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = pxConstList->pxIndex; _8 = _7->pxNext; pxConstList->pxIndex = _8; : # DEBUG BEGIN_STMT _9 = pxConstList->pxIndex; _10 = _9->pvOwner; pxCurrentTCB = _10; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxTopReadyPriority = uxTopPriority; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT return; } xTaskIncrementTick () { struct ListItem_t * const pxIndex; struct List_t * const pxList; struct List_t * const pxList; struct List_t * pxTemp; const TickType_t xConstTickCount; BaseType_t xSwitchRequired; TickType_t xItemValue; struct TCB_t * pxTCB; BaseType_t D.7919; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xSwitchRequired = 0; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.79_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.79_1 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xTickCount.80_2 = xTickCount; xConstTickCount = xTickCount.80_2 + 1; # DEBUG BEGIN_STMT xTickCount = xConstTickCount; # DEBUG BEGIN_STMT if (xConstTickCount == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxDelayedTaskList.81_3 = pxDelayedTaskList; _4 = pxDelayedTaskList.81_3->uxNumberOfItems; if (_4 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTemp = pxDelayedTaskList; # DEBUG BEGIN_STMT pxOverflowDelayedTaskList.82_5 = pxOverflowDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList.82_5; # DEBUG BEGIN_STMT pxOverflowDelayedTaskList = pxTemp; # DEBUG BEGIN_STMT xNumOfOverflows.83_6 = xNumOfOverflows; _7 = xNumOfOverflows.83_6 + 1; xNumOfOverflows = _7; # DEBUG BEGIN_STMT prvResetNextTaskUnblockTime (); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xNextTaskUnblockTime.84_8 = xNextTaskUnblockTime; if (xConstTickCount >= xNextTaskUnblockTime.84_8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxDelayedTaskList.85_9 = pxDelayedTaskList; _10 = pxDelayedTaskList.85_9->uxNumberOfItems; if (_10 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xNextTaskUnblockTime = 4294967295; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT pxDelayedTaskList.86_11 = pxDelayedTaskList; _12 = pxDelayedTaskList.86_11->xListEnd.pxNext; pxTCB = _12->pvOwner; # DEBUG BEGIN_STMT xItemValue = pxTCB->xStateListItem.xItemValue; # DEBUG BEGIN_STMT if (xConstTickCount < xItemValue) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xNextTaskUnblockTime = xItemValue; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxList = pxTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _13 = pxTCB->xStateListItem.pxNext; _14 = pxTCB->xStateListItem.pxPrevious; _13->pxPrevious = _14; # DEBUG BEGIN_STMT _15 = pxTCB->xStateListItem.pxPrevious; _16 = pxTCB->xStateListItem.pxNext; _15->pxNext = _16; # DEBUG BEGIN_STMT _17 = pxList->pxIndex; _18 = &pxTCB->xStateListItem; if (_17 == _18) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _19 = pxTCB->xStateListItem.pxPrevious; pxList->pxIndex = _19; : # DEBUG BEGIN_STMT pxTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _20 = pxList->uxNumberOfItems; _21 = _20 + 4294967295; pxList->uxNumberOfItems = _21; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _22 = pxTCB->xEventListItem.pvContainer; if (_22 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxList = pxTCB->xEventListItem.pvContainer; # DEBUG BEGIN_STMT _23 = pxTCB->xEventListItem.pxNext; _24 = pxTCB->xEventListItem.pxPrevious; _23->pxPrevious = _24; # DEBUG BEGIN_STMT _25 = pxTCB->xEventListItem.pxPrevious; _26 = pxTCB->xEventListItem.pxNext; _25->pxNext = _26; # DEBUG BEGIN_STMT _27 = pxList->pxIndex; _28 = &pxTCB->xEventListItem; if (_27 == _28) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _29 = pxTCB->xEventListItem.pxPrevious; pxList->pxIndex = _29; : # DEBUG BEGIN_STMT pxTCB->xEventListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _30 = pxList->uxNumberOfItems; _31 = _30 + 4294967295; pxList->uxNumberOfItems = _31; # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _32 = pxTCB->uxPriority; uxTopReadyPriority.87_33 = uxTopReadyPriority; if (_32 > uxTopReadyPriority.87_33) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _34 = pxTCB->uxPriority; uxTopReadyPriority = _34; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _35 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_35].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _36 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _36; # DEBUG BEGIN_STMT _37 = pxIndex->pxPrevious; _38 = &pxTCB->xStateListItem; _37->pxNext = _38; # DEBUG BEGIN_STMT _39 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _39; # DEBUG BEGIN_STMT _40 = pxTCB->uxPriority; _41 = &pxReadyTasksLists[_40]; pxTCB->xStateListItem.pvContainer = _41; # DEBUG BEGIN_STMT _42 = pxTCB->uxPriority; _43 = pxReadyTasksLists[_42].uxNumberOfItems; _44 = _43 + 1; pxReadyTasksLists[_42].uxNumberOfItems = _44; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _45 = pxTCB->uxPriority; pxCurrentTCB.88_46 = pxCurrentTCB; _47 = pxCurrentTCB.88_46->uxPriority; if (_45 >= _47) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xSwitchRequired = 1; goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.89_48 = pxCurrentTCB; _49 = pxCurrentTCB.89_48->uxPriority; _50 = pxReadyTasksLists[_49].uxNumberOfItems; if (_50 > 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xSwitchRequired = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xYieldPending.90_51 = xYieldPending; if (xYieldPending.90_51 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xSwitchRequired = 1; goto ; [INV] : # DEBUG BEGIN_STMT xPendedTicks.91_52 = xPendedTicks; _53 = xPendedTicks.91_52 + 1; xPendedTicks = _53; : # DEBUG BEGIN_STMT D.7919 = xSwitchRequired; return D.7919; } xTaskAbortDelay (struct tskTaskControlBlock * xTask) { struct ListItem_t * const pxIndex; BaseType_t xReturn; struct TCB_t * pxTCB; BaseType_t D.7885; : # DEBUG BEGIN_STMT pxTCB = xTask; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vTaskSuspendAll (); # DEBUG BEGIN_STMT _1 = eTaskGetState (xTask); if (_1 == 2) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 1; # DEBUG BEGIN_STMT _2 = &pxTCB->xStateListItem; uxListRemove (_2); # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT _3 = pxTCB->xEventListItem.pvContainer; if (_3 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = &pxTCB->xEventListItem; uxListRemove (_4); # DEBUG BEGIN_STMT pxTCB->ucDelayAborted = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _5 = pxTCB->uxPriority; uxTopReadyPriority.77_6 = uxTopReadyPriority; if (_5 > uxTopReadyPriority.77_6) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = pxTCB->uxPriority; uxTopReadyPriority = _7; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _8 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_8].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _9 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _9; # DEBUG BEGIN_STMT _10 = pxIndex->pxPrevious; _11 = &pxTCB->xStateListItem; _10->pxNext = _11; # DEBUG BEGIN_STMT _12 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _12; # DEBUG BEGIN_STMT _13 = pxTCB->uxPriority; _14 = &pxReadyTasksLists[_13]; pxTCB->xStateListItem.pvContainer = _14; # DEBUG BEGIN_STMT _15 = pxTCB->uxPriority; _16 = pxReadyTasksLists[_15].uxNumberOfItems; _17 = _16 + 1; pxReadyTasksLists[_15].uxNumberOfItems = _17; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _18 = pxTCB->uxPriority; pxCurrentTCB.78_19 = pxCurrentTCB; _20 = pxCurrentTCB.78_19->uxPriority; if (_18 > _20) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldPending = 1; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 0; : # DEBUG BEGIN_STMT xTaskResumeAll (); # DEBUG BEGIN_STMT D.7885 = xReturn; return D.7885; } xTaskCatchUpTicks (TickType_t xTicksToCatchUp) { BaseType_t xYieldOccurred; BaseType_t D.7870; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.75_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.75_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vTaskSuspendAll (); # DEBUG BEGIN_STMT xPendedTicks.76_2 = xPendedTicks; _3 = xTicksToCatchUp + xPendedTicks.76_2; xPendedTicks = _3; # DEBUG BEGIN_STMT xYieldOccurred = xTaskResumeAll (); # DEBUG BEGIN_STMT D.7870 = xYieldOccurred; return D.7870; } uxTaskGetSystemState (struct TaskStatus_t * const pxTaskStatusArray, const UBaseType_t uxArraySize, uint32_t * const pulTotalRunTime) { UBaseType_t uxQueue; UBaseType_t uxTask; UBaseType_t D.7857; long unsigned int D.7853; long unsigned int D.7852; long unsigned int D.7851; long unsigned int D.7850; long unsigned int D.7849; : # DEBUG BEGIN_STMT uxTask = 0; uxQueue = 5; # DEBUG BEGIN_STMT vTaskSuspendAll (); # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.72_1 = uxCurrentNumberOfTasks; if (uxArraySize >= uxCurrentNumberOfTasks.72_1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxQueue = uxQueue + 4294967295; # DEBUG BEGIN_STMT _2 = uxTask * 36; _3 = pxTaskStatusArray + _2; _4 = &pxReadyTasksLists[uxQueue]; D.7849 = prvListTasksWithinSingleList (_3, _4, 1); uxTask = D.7849 + uxTask; # DEBUG BEGIN_STMT if (uxQueue != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _5 = uxTask * 36; _6 = pxTaskStatusArray + _5; pxDelayedTaskList.73_7 = pxDelayedTaskList; D.7850 = prvListTasksWithinSingleList (_6, pxDelayedTaskList.73_7, 2); uxTask = D.7850 + uxTask; # DEBUG BEGIN_STMT _8 = uxTask * 36; _9 = pxTaskStatusArray + _8; pxOverflowDelayedTaskList.74_10 = pxOverflowDelayedTaskList; D.7851 = prvListTasksWithinSingleList (_9, pxOverflowDelayedTaskList.74_10, 2); uxTask = D.7851 + uxTask; # DEBUG BEGIN_STMT _11 = uxTask * 36; _12 = pxTaskStatusArray + _11; D.7852 = prvListTasksWithinSingleList (_12, &xTasksWaitingTermination, 4); uxTask = D.7852 + uxTask; # DEBUG BEGIN_STMT _13 = uxTask * 36; _14 = pxTaskStatusArray + _13; D.7853 = prvListTasksWithinSingleList (_14, &xSuspendedTaskList, 3); uxTask = D.7853 + uxTask; # DEBUG BEGIN_STMT if (pulTotalRunTime != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT *pulTotalRunTime = 0; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xTaskResumeAll (); # DEBUG BEGIN_STMT D.7857 = uxTask; return D.7857; } xTaskGetHandle (const char * pcNameToQuery) { struct TCB_t * pxTCB; UBaseType_t uxQueue; struct tskTaskControlBlock * D.7828; : # DEBUG BEGIN_STMT uxQueue = 5; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = strlen (pcNameToQuery); if (_1 > 9) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vTaskSuspendAll (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxQueue = uxQueue + 4294967295; # DEBUG BEGIN_STMT _2 = &pxReadyTasksLists[uxQueue]; pxTCB = prvSearchForNameWithinSingleList (_2, pcNameToQuery); # DEBUG BEGIN_STMT if (pxTCB != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (uxQueue != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxDelayedTaskList.70_3 = pxDelayedTaskList; pxTCB = prvSearchForNameWithinSingleList (pxDelayedTaskList.70_3, pcNameToQuery); : # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxOverflowDelayedTaskList.71_4 = pxOverflowDelayedTaskList; pxTCB = prvSearchForNameWithinSingleList (pxOverflowDelayedTaskList.71_4, pcNameToQuery); : # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB = prvSearchForNameWithinSingleList (&xSuspendedTaskList, pcNameToQuery); : # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB = prvSearchForNameWithinSingleList (&xTasksWaitingTermination, pcNameToQuery); : # DEBUG BEGIN_STMT xTaskResumeAll (); # DEBUG BEGIN_STMT D.7828 = pxTCB; return D.7828; } prvSearchForNameWithinSingleList (struct List_t * pxList, const char * pcNameToQuery) { struct List_t * const pxConstList; struct List_t * const pxConstList; BaseType_t xBreakLoop; char cNextChar; UBaseType_t x; struct TCB_t * pxReturn; struct TCB_t * pxFirstTCB; struct TCB_t * pxNextTCB; struct TCB_t * D.7845; : # DEBUG BEGIN_STMT pxReturn = 0B; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = pxList->uxNumberOfItems; if (_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxConstList = pxList; # DEBUG BEGIN_STMT _2 = pxConstList->pxIndex; _3 = _2->pxNext; pxConstList->pxIndex = _3; # DEBUG BEGIN_STMT _4 = pxConstList->pxIndex; _5 = &pxConstList->xListEnd; if (_4 == _5) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = pxConstList->pxIndex; _7 = _6->pxNext; pxConstList->pxIndex = _7; : # DEBUG BEGIN_STMT _8 = pxConstList->pxIndex; pxFirstTCB = _8->pvOwner; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxConstList = pxList; # DEBUG BEGIN_STMT _9 = pxConstList->pxIndex; _10 = _9->pxNext; pxConstList->pxIndex = _10; # DEBUG BEGIN_STMT _11 = pxConstList->pxIndex; _12 = &pxConstList->xListEnd; if (_11 == _12) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = pxConstList->pxIndex; _14 = _13->pxNext; pxConstList->pxIndex = _14; : # DEBUG BEGIN_STMT _15 = pxConstList->pxIndex; pxNextTCB = _15->pvOwner; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xBreakLoop = 0; # DEBUG BEGIN_STMT x = 0; goto ; [INV] : # DEBUG BEGIN_STMT cNextChar = pxNextTCB->pcTaskName[x]; # DEBUG BEGIN_STMT _16 = pcNameToQuery + x; _17 = *_16; if (cNextChar != _17) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xBreakLoop = 1; goto ; [INV] : # DEBUG BEGIN_STMT if (cNextChar == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxReturn = pxNextTCB; # DEBUG BEGIN_STMT xBreakLoop = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xBreakLoop != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT x = x + 1; : # DEBUG BEGIN_STMT if (x <= 9) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (pxReturn != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (pxNextTCB != pxFirstTCB) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7845 = pxReturn; return D.7845; } pcTaskGetName (struct tskTaskControlBlock * xTaskToQuery) { struct TCB_t * pxTCB; char * D.7815; struct TCB_t * iftmp.69; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTaskToQuery == 0B) goto ; [INV] else goto ; [INV] : iftmp.69 = pxCurrentTCB; goto ; [INV] : iftmp.69 = xTaskToQuery; : pxTCB = iftmp.69; # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7815 = &pxTCB->pcTaskName[0]; return D.7815; } uxTaskGetNumberOfTasks () { UBaseType_t D.7807; : # DEBUG BEGIN_STMT D.7807 = uxCurrentNumberOfTasks; return D.7807; } xTaskGetTickCountFromISR () { UBaseType_t uxSavedInterruptStatus; TickType_t xReturn; TickType_t D.7805; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortValidateInterruptPriority (); # DEBUG BEGIN_STMT uxSavedInterruptStatus = 0; # DEBUG BEGIN_STMT xReturn = xTickCount; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7805 = xReturn; return D.7805; } xTaskGetTickCount () { TickType_t xTicks; TickType_t D.7803; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xTicks = xTickCount; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7803 = xTicks; return D.7803; } xTaskResumeAll () { TickType_t xPendedCounts; struct ListItem_t * const pxIndex; struct List_t * const pxList; struct List_t * const pxList; BaseType_t xAlreadyYielded; struct TCB_t * pxTCB; BaseType_t D.7801; : # DEBUG BEGIN_STMT pxTCB = 0B; # DEBUG BEGIN_STMT xAlreadyYielded = 0; # DEBUG BEGIN_STMT uxSchedulerSuspended.62_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.62_1 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT uxSchedulerSuspended.63_2 = uxSchedulerSuspended; _3 = uxSchedulerSuspended.63_2 + 4294967295; uxSchedulerSuspended = _3; # DEBUG BEGIN_STMT uxSchedulerSuspended.64_4 = uxSchedulerSuspended; if (uxSchedulerSuspended.64_4 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.65_5 = uxCurrentNumberOfTasks; if (uxCurrentNumberOfTasks.65_5 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = xPendingReadyList.xListEnd.pxNext; pxTCB = _6->pvOwner; # DEBUG BEGIN_STMT pxList = pxTCB->xEventListItem.pvContainer; # DEBUG BEGIN_STMT _7 = pxTCB->xEventListItem.pxNext; _8 = pxTCB->xEventListItem.pxPrevious; _7->pxPrevious = _8; # DEBUG BEGIN_STMT _9 = pxTCB->xEventListItem.pxPrevious; _10 = pxTCB->xEventListItem.pxNext; _9->pxNext = _10; # DEBUG BEGIN_STMT _11 = pxList->pxIndex; _12 = &pxTCB->xEventListItem; if (_11 == _12) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _13 = pxTCB->xEventListItem.pxPrevious; pxList->pxIndex = _13; : # DEBUG BEGIN_STMT pxTCB->xEventListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _14 = pxList->uxNumberOfItems; _15 = _14 + 4294967295; pxList->uxNumberOfItems = _15; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT __asm__ __volatile__("" : : : "memory"); # DEBUG BEGIN_STMT pxList = pxTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT _16 = pxTCB->xStateListItem.pxNext; _17 = pxTCB->xStateListItem.pxPrevious; _16->pxPrevious = _17; # DEBUG BEGIN_STMT _18 = pxTCB->xStateListItem.pxPrevious; _19 = pxTCB->xStateListItem.pxNext; _18->pxNext = _19; # DEBUG BEGIN_STMT _20 = pxList->pxIndex; _21 = &pxTCB->xStateListItem; if (_20 == _21) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _22 = pxTCB->xStateListItem.pxPrevious; pxList->pxIndex = _22; : # DEBUG BEGIN_STMT pxTCB->xStateListItem.pvContainer = 0B; # DEBUG BEGIN_STMT _23 = pxList->uxNumberOfItems; _24 = _23 + 4294967295; pxList->uxNumberOfItems = _24; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _25 = pxTCB->uxPriority; uxTopReadyPriority.66_26 = uxTopReadyPriority; if (_25 > uxTopReadyPriority.66_26) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _27 = pxTCB->uxPriority; uxTopReadyPriority = _27; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _28 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_28].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _29 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _29; # DEBUG BEGIN_STMT _30 = pxIndex->pxPrevious; _31 = &pxTCB->xStateListItem; _30->pxNext = _31; # DEBUG BEGIN_STMT _32 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _32; # DEBUG BEGIN_STMT _33 = pxTCB->uxPriority; _34 = &pxReadyTasksLists[_33]; pxTCB->xStateListItem.pvContainer = _34; # DEBUG BEGIN_STMT _35 = pxTCB->uxPriority; _36 = pxReadyTasksLists[_35].uxNumberOfItems; _37 = _36 + 1; pxReadyTasksLists[_35].uxNumberOfItems = _37; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _38 = pxTCB->uxPriority; pxCurrentTCB.67_39 = pxCurrentTCB; _40 = pxCurrentTCB.67_39->uxPriority; if (_38 >= _40) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldPending = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _41 = xPendingReadyList.uxNumberOfItems; if (_41 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (pxTCB != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT prvResetNextTaskUnblockTime (); : # DEBUG BEGIN_STMT xPendedCounts = xPendedTicks; # DEBUG BEGIN_STMT if (xPendedCounts != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _42 = xTaskIncrementTick (); if (_42 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldPending = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xPendedCounts = xPendedCounts + 4294967295; # DEBUG BEGIN_STMT if (xPendedCounts != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xPendedTicks = 0; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xYieldPending.68_43 = xYieldPending; if (xYieldPending.68_43 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xAlreadyYielded = 1; # DEBUG BEGIN_STMT _44 = 3758157060B; *_44 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.7801 = xAlreadyYielded; return D.7801; } vTaskSuspendAll () { : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.61_1 = uxSchedulerSuspended; _2 = uxSchedulerSuspended.61_1 + 1; uxSchedulerSuspended = _2; # DEBUG BEGIN_STMT __asm__ __volatile__("" : : : "memory"); return; } vTaskEndScheduler () { : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); # DEBUG BEGIN_STMT xSchedulerRunning = 0; # DEBUG BEGIN_STMT vPortEndScheduler (); return; } vTaskStartScheduler () { BaseType_t xReturn; long unsigned int vol.57; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xReturn = xTaskCreate (prvIdleTask, "IDLE", 90, 0B, 0, &xIdleTaskHandle); # DEBUG BEGIN_STMT if (xReturn == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = xTimerCreateTimerTask (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xReturn == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); # DEBUG BEGIN_STMT xNextTaskUnblockTime = 4294967295; # DEBUG BEGIN_STMT xSchedulerRunning = 1; # DEBUG BEGIN_STMT xTickCount = 0; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = xPortStartScheduler (); goto ; [INV] : # DEBUG BEGIN_STMT if (xReturn == -1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vol.57 = uxTopUsedPriority; return; } xTaskResumeFromISR (struct tskTaskControlBlock * xTaskToResume) { struct ListItem_t * const pxIndex; UBaseType_t uxSavedInterruptStatus; struct TCB_t * const pxTCB; BaseType_t xYieldRequired; BaseType_t D.7757; : # DEBUG BEGIN_STMT xYieldRequired = 0; # DEBUG BEGIN_STMT pxTCB = xTaskToResume; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTaskToResume == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortValidateInterruptPriority (); # DEBUG BEGIN_STMT uxSavedInterruptStatus = ulPortRaiseBASEPRI (); # DEBUG BEGIN_STMT _1 = prvTaskIsTaskSuspended (pxTCB); if (_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.54_2 = uxSchedulerSuspended; if (uxSchedulerSuspended.54_2 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _3 = pxTCB->uxPriority; pxCurrentTCB.55_4 = pxCurrentTCB; _5 = pxCurrentTCB.55_4->uxPriority; if (_3 >= _5) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldRequired = 1; # DEBUG BEGIN_STMT xYieldPending = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _6 = &pxTCB->xStateListItem; uxListRemove (_6); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _7 = pxTCB->uxPriority; uxTopReadyPriority.56_8 = uxTopReadyPriority; if (_7 > uxTopReadyPriority.56_8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = pxTCB->uxPriority; uxTopReadyPriority = _9; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _10 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_10].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _11 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _11; # DEBUG BEGIN_STMT _12 = pxIndex->pxPrevious; _13 = &pxTCB->xStateListItem; _12->pxNext = _13; # DEBUG BEGIN_STMT _14 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _14; # DEBUG BEGIN_STMT _15 = pxTCB->uxPriority; _16 = &pxReadyTasksLists[_15]; pxTCB->xStateListItem.pvContainer = _16; # DEBUG BEGIN_STMT _17 = pxTCB->uxPriority; _18 = pxReadyTasksLists[_17].uxNumberOfItems; _19 = _18 + 1; pxReadyTasksLists[_17].uxNumberOfItems = _19; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT _20 = &pxTCB->xEventListItem; vListInsertEnd (&xPendingReadyList, _20); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortSetBASEPRI (uxSavedInterruptStatus); # DEBUG BEGIN_STMT D.7757 = xYieldRequired; return D.7757; } vTaskResume (struct tskTaskControlBlock * xTaskToResume) { struct ListItem_t * const pxIndex; struct TCB_t * const pxTCB; : # DEBUG BEGIN_STMT pxTCB = xTaskToResume; # DEBUG BEGIN_STMT if (xTaskToResume == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.51_1 = pxCurrentTCB; if (pxTCB != pxCurrentTCB.51_1) goto ; [INV] else goto ; [INV] : if (pxTCB != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT _2 = prvTaskIsTaskSuspended (pxTCB); if (_2 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _3 = &pxTCB->xStateListItem; uxListRemove (_3); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _4 = pxTCB->uxPriority; uxTopReadyPriority.52_5 = uxTopReadyPriority; if (_4 > uxTopReadyPriority.52_5) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _6 = pxTCB->uxPriority; uxTopReadyPriority = _6; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _7 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_7].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _8 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _8; # DEBUG BEGIN_STMT _9 = pxIndex->pxPrevious; _10 = &pxTCB->xStateListItem; _9->pxNext = _10; # DEBUG BEGIN_STMT _11 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _11; # DEBUG BEGIN_STMT _12 = pxTCB->uxPriority; _13 = &pxReadyTasksLists[_12]; pxTCB->xStateListItem.pvContainer = _13; # DEBUG BEGIN_STMT _14 = pxTCB->uxPriority; _15 = pxReadyTasksLists[_14].uxNumberOfItems; _16 = _15 + 1; pxReadyTasksLists[_14].uxNumberOfItems = _16; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _17 = pxTCB->uxPriority; pxCurrentTCB.53_18 = pxCurrentTCB; _19 = pxCurrentTCB.53_18->uxPriority; if (_17 >= _19) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _20 = 3758157060B; *_20 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); : # DEBUG BEGIN_STMT return; } prvTaskIsTaskSuspended (struct tskTaskControlBlock * const xTask) { const struct TCB_t * const pxTCB; BaseType_t xReturn; BaseType_t D.7742; : # DEBUG BEGIN_STMT xReturn = 0; # DEBUG BEGIN_STMT pxTCB = xTask; # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = pxTCB->xStateListItem.pvContainer; if (_1 == &xSuspendedTaskList) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _2 = pxTCB->xEventListItem.pvContainer; if (_2 != &xPendingReadyList) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _3 = pxTCB->xEventListItem.pvContainer; if (_3 == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xReturn = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7742 = xReturn; return D.7742; } vTaskSuspend (struct tskTaskControlBlock * xTaskToSuspend) { BaseType_t x; struct TCB_t * pxTCB; struct TCB_t * iftmp.45; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT if (xTaskToSuspend == 0B) goto ; [INV] else goto ; [INV] : iftmp.45 = pxCurrentTCB; goto ; [INV] : iftmp.45 = xTaskToSuspend; : pxTCB = iftmp.45; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = &pxTCB->xStateListItem; _2 = uxListRemove (_1); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _3 = pxTCB->xEventListItem.pvContainer; if (_3 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = &pxTCB->xEventListItem; uxListRemove (_4); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _5 = &pxTCB->xStateListItem; vListInsertEnd (&xSuspendedTaskList, _5); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT x = 0; goto ; [INV] : # DEBUG BEGIN_STMT _6 = pxTCB->ucNotifyState[x]; if (_6 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB->ucNotifyState[x] = 0; : # DEBUG BEGIN_STMT x = x + 1; : # DEBUG BEGIN_STMT if (x <= 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT xSchedulerRunning.46_7 = xSchedulerRunning; if (xSchedulerRunning.46_7 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT prvResetNextTaskUnblockTime (); # DEBUG BEGIN_STMT vPortExitCritical (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.47_8 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.47_8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xSchedulerRunning.48_9 = xSchedulerRunning; if (xSchedulerRunning.48_9 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxSchedulerSuspended.49_10 = uxSchedulerSuspended; if (uxSchedulerSuspended.49_10 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _11 = 3758157060B; *_11 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT _12 = xSuspendedTaskList.uxNumberOfItems; uxCurrentNumberOfTasks.50_13 = uxCurrentNumberOfTasks; if (_12 == uxCurrentNumberOfTasks.50_13) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB = 0B; goto ; [INV] : # DEBUG BEGIN_STMT vTaskSwitchContext (); : # DEBUG BEGIN_STMT return; } vTaskPrioritySet (struct tskTaskControlBlock * xTask, UBaseType_t uxNewPriority) { struct ListItem_t * const pxIndex; BaseType_t xYieldRequired; UBaseType_t uxPriorityUsedOnEntry; UBaseType_t uxCurrentBasePriority; struct TCB_t * pxTCB; struct TCB_t * iftmp.40; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xYieldRequired = 0; # DEBUG BEGIN_STMT if (uxNewPriority > 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxNewPriority > 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxNewPriority = 4; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.40 = pxCurrentTCB; goto ; [INV] : iftmp.40 = xTask; : pxTCB = iftmp.40; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxCurrentBasePriority = pxTCB->uxBasePriority; # DEBUG BEGIN_STMT if (uxCurrentBasePriority != uxNewPriority) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT if (uxNewPriority > uxCurrentBasePriority) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.41_1 = pxCurrentTCB; if (pxTCB != pxCurrentTCB.41_1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.42_2 = pxCurrentTCB; _3 = pxCurrentTCB.42_2->uxPriority; if (uxNewPriority >= _3) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldRequired = 1; goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.43_4 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.43_4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xYieldRequired = 1; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxPriorityUsedOnEntry = pxTCB->uxPriority; # DEBUG BEGIN_STMT _5 = pxTCB->uxBasePriority; _6 = pxTCB->uxPriority; if (_5 == _6) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxTCB->uxPriority = uxNewPriority; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->uxBasePriority = uxNewPriority; # DEBUG BEGIN_STMT _7 = pxTCB->xEventListItem.xItemValue; _8 = (signed int) _7; if (_8 >= 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _9 = 5 - uxNewPriority; pxTCB->xEventListItem.xItemValue = _9; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _10 = pxTCB->xStateListItem.pvContainer; _11 = &pxReadyTasksLists[uxPriorityUsedOnEntry]; if (_10 == _11) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _12 = &pxTCB->xStateListItem; _13 = uxListRemove (_12); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _14 = pxTCB->uxPriority; uxTopReadyPriority.44_15 = uxTopReadyPriority; if (_14 > uxTopReadyPriority.44_15) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _16 = pxTCB->uxPriority; uxTopReadyPriority = _16; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _17 = pxTCB->uxPriority; pxIndex = pxReadyTasksLists[_17].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _18 = pxIndex->pxPrevious; pxTCB->xStateListItem.pxPrevious = _18; # DEBUG BEGIN_STMT _19 = pxIndex->pxPrevious; _20 = &pxTCB->xStateListItem; _19->pxNext = _20; # DEBUG BEGIN_STMT _21 = &pxTCB->xStateListItem; pxIndex->pxPrevious = _21; # DEBUG BEGIN_STMT _22 = pxTCB->uxPriority; _23 = &pxReadyTasksLists[_22]; pxTCB->xStateListItem.pvContainer = _23; # DEBUG BEGIN_STMT _24 = pxTCB->uxPriority; _25 = pxReadyTasksLists[_24].uxNumberOfItems; _26 = _25 + 1; pxReadyTasksLists[_24].uxNumberOfItems = _26; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xYieldRequired != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _27 = 3758157060B; *_27 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); return; } uxTaskPriorityGetFromISR (struct tskTaskControlBlock * const xTask) { UBaseType_t uxSavedInterruptState; UBaseType_t uxReturn; const struct TCB_t * pxTCB; UBaseType_t D.7646; const struct TCB_t * iftmp.39; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortValidateInterruptPriority (); # DEBUG BEGIN_STMT uxSavedInterruptState = ulPortRaiseBASEPRI (); # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.39 = pxCurrentTCB; goto ; [INV] : iftmp.39 = xTask; : pxTCB = iftmp.39; # DEBUG BEGIN_STMT uxReturn = pxTCB->uxPriority; # DEBUG BEGIN_STMT vPortSetBASEPRI (uxSavedInterruptState); # DEBUG BEGIN_STMT D.7646 = uxReturn; return D.7646; } uxTaskPriorityGet (struct tskTaskControlBlock * const xTask) { UBaseType_t uxReturn; const struct TCB_t * pxTCB; UBaseType_t D.7640; const struct TCB_t * iftmp.38; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT if (xTask == 0B) goto ; [INV] else goto ; [INV] : iftmp.38 = pxCurrentTCB; goto ; [INV] : iftmp.38 = xTask; : pxTCB = iftmp.38; # DEBUG BEGIN_STMT uxReturn = pxTCB->uxPriority; # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT D.7640 = uxReturn; return D.7640; } eTaskGetState (struct tskTaskControlBlock * xTask) { BaseType_t x; const struct TCB_t * const pxTCB; const struct List_t * pxOverflowedDelayedList; const struct List_t * pxDelayedList; const struct List_t * pxStateList; eTaskState eReturn; eTaskState D.7634; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxTCB = xTask; # DEBUG BEGIN_STMT if (pxTCB == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxCurrentTCB.37_1 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.37_1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eReturn = 0; goto ; [INV] : # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT pxStateList = pxTCB->xStateListItem.pvContainer; # DEBUG BEGIN_STMT pxDelayedList = pxDelayedTaskList; # DEBUG BEGIN_STMT pxOverflowedDelayedList = pxOverflowDelayedTaskList; # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT if (pxStateList == pxDelayedList) goto ; [INV] else goto ; [INV] : if (pxStateList == pxOverflowedDelayedList) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eReturn = 2; goto ; [INV] : # DEBUG BEGIN_STMT if (pxStateList == &xSuspendedTaskList) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _2 = pxTCB->xEventListItem.pvContainer; if (_2 == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT eReturn = 3; # DEBUG BEGIN_STMT x = 0; goto ; [INV] : # DEBUG BEGIN_STMT _3 = pxTCB->ucNotifyState[x]; if (_3 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eReturn = 2; # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT x = x + 1; : # DEBUG BEGIN_STMT if (x <= 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eReturn = 2; goto ; [INV] : # DEBUG BEGIN_STMT if (pxStateList == &xTasksWaitingTermination) goto ; [INV] else goto ; [INV] : if (pxStateList == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT eReturn = 4; goto ; [INV] : # DEBUG BEGIN_STMT eReturn = 1; : # DEBUG BEGIN_STMT D.7634 = eReturn; return D.7634; } vTaskDelay (const TickType_t xTicksToDelay) { BaseType_t xAlreadyYielded; : # DEBUG BEGIN_STMT xAlreadyYielded = 0; # DEBUG BEGIN_STMT if (xTicksToDelay != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxSchedulerSuspended.36_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.36_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vTaskSuspendAll (); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT prvAddCurrentTaskToDelayedList (xTicksToDelay, 0); # DEBUG BEGIN_STMT xAlreadyYielded = xTaskResumeAll (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xAlreadyYielded == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _2 = 3758157060B; *_2 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT return; } xTaskDelayUntil (TickType_t * const pxPreviousWakeTime, const TickType_t xTimeIncrement) { const TickType_t xConstTickCount; BaseType_t xShouldDelay; BaseType_t xAlreadyYielded; TickType_t xTimeToWake; BaseType_t D.7590; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xShouldDelay = 0; # DEBUG BEGIN_STMT if (pxPreviousWakeTime == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (xTimeIncrement == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxSchedulerSuspended.22_1 = uxSchedulerSuspended; if (uxSchedulerSuspended.22_1 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vTaskSuspendAll (); # DEBUG BEGIN_STMT xConstTickCount = xTickCount; # DEBUG BEGIN_STMT _2 = *pxPreviousWakeTime; xTimeToWake = xTimeIncrement + _2; # DEBUG BEGIN_STMT _3 = *pxPreviousWakeTime; if (xConstTickCount < _3) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = *pxPreviousWakeTime; if (xTimeToWake < _4) goto ; [INV] else goto ; [INV] : if (xTimeToWake > xConstTickCount) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xShouldDelay = 1; goto ; [INV] : # DEBUG BEGIN_STMT _5 = *pxPreviousWakeTime; if (xTimeToWake < _5) goto ; [INV] else goto ; [INV] : if (xTimeToWake > xConstTickCount) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT xShouldDelay = 1; : # DEBUG BEGIN_STMT *pxPreviousWakeTime = xTimeToWake; # DEBUG BEGIN_STMT if (xShouldDelay != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _6 = xTimeToWake - xConstTickCount; prvAddCurrentTaskToDelayedList (_6, 0); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT xAlreadyYielded = xTaskResumeAll (); # DEBUG BEGIN_STMT if (xAlreadyYielded == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _7 = 3758157060B; *_7 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT D.7590 = xShouldDelay; return D.7590; } vTaskDelete (struct tskTaskControlBlock * xTaskToDelete) { struct TCB_t * pxTCB; struct TCB_t * iftmp.12; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT if (xTaskToDelete == 0B) goto ; [INV] else goto ; [INV] : iftmp.12 = pxCurrentTCB; goto ; [INV] : iftmp.12 = xTaskToDelete; : pxTCB = iftmp.12; # DEBUG BEGIN_STMT _1 = &pxTCB->xStateListItem; _2 = uxListRemove (_1); # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _3 = pxTCB->xEventListItem.pvContainer; if (_3 != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _4 = &pxTCB->xEventListItem; uxListRemove (_4); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxTaskNumber.13_5 = uxTaskNumber; _6 = uxTaskNumber.13_5 + 1; uxTaskNumber = _6; # DEBUG BEGIN_STMT pxCurrentTCB.14_7 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.14_7) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _8 = &pxTCB->xStateListItem; vListInsertEnd (&xTasksWaitingTermination, _8); # DEBUG BEGIN_STMT uxDeletedTasksWaitingCleanUp.15_9 = uxDeletedTasksWaitingCleanUp; _10 = uxDeletedTasksWaitingCleanUp.15_9 + 1; uxDeletedTasksWaitingCleanUp = _10; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.16_11 = uxCurrentNumberOfTasks; _12 = uxCurrentNumberOfTasks.16_11 + 4294967295; uxCurrentNumberOfTasks = _12; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT prvDeleteTCB (pxTCB); # DEBUG BEGIN_STMT prvResetNextTaskUnblockTime (); : # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT xSchedulerRunning.17_13 = xSchedulerRunning; if (xSchedulerRunning.17_13 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.18_14 = pxCurrentTCB; if (pxTCB == pxCurrentTCB.18_14) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxSchedulerSuspended.19_15 = uxSchedulerSuspended; if (uxSchedulerSuspended.19_15 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _16 = 3758157060B; *_16 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT return; } prvAddNewTaskToReadyList (struct TCB_t * pxNewTCB) { struct ListItem_t * const pxIndex; : # DEBUG BEGIN_STMT vPortEnterCritical (); # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.2_1 = uxCurrentNumberOfTasks; _2 = uxCurrentNumberOfTasks.2_1 + 1; uxCurrentNumberOfTasks = _2; # DEBUG BEGIN_STMT pxCurrentTCB.3_3 = pxCurrentTCB; if (pxCurrentTCB.3_3 == 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB = pxNewTCB; # DEBUG BEGIN_STMT uxCurrentNumberOfTasks.4_4 = uxCurrentNumberOfTasks; if (uxCurrentNumberOfTasks.4_4 == 1) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT prvInitialiseTaskLists (); goto ; [INV] : # DEBUG BEGIN_STMT xSchedulerRunning.5_5 = xSchedulerRunning; if (xSchedulerRunning.5_5 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.6_6 = pxCurrentTCB; _7 = pxCurrentTCB.6_6->uxPriority; _8 = pxNewTCB->uxPriority; if (_7 <= _8) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB = pxNewTCB; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT uxTaskNumber.7_9 = uxTaskNumber; _10 = uxTaskNumber.7_9 + 1; uxTaskNumber = _10; # DEBUG BEGIN_STMT uxTaskNumber.8_11 = uxTaskNumber; pxNewTCB->uxTCBNumber = uxTaskNumber.8_11; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _12 = pxNewTCB->uxPriority; uxTopReadyPriority.9_13 = uxTopReadyPriority; if (_12 > uxTopReadyPriority.9_13) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _14 = pxNewTCB->uxPriority; uxTopReadyPriority = _14; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _15 = pxNewTCB->uxPriority; pxIndex = pxReadyTasksLists[_15].pxIndex; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxNewTCB->xStateListItem.pxNext = pxIndex; # DEBUG BEGIN_STMT _16 = pxIndex->pxPrevious; pxNewTCB->xStateListItem.pxPrevious = _16; # DEBUG BEGIN_STMT _17 = pxIndex->pxPrevious; _18 = &pxNewTCB->xStateListItem; _17->pxNext = _18; # DEBUG BEGIN_STMT _19 = &pxNewTCB->xStateListItem; pxIndex->pxPrevious = _19; # DEBUG BEGIN_STMT _20 = pxNewTCB->uxPriority; _21 = &pxReadyTasksLists[_20]; pxNewTCB->xStateListItem.pvContainer = _21; # DEBUG BEGIN_STMT _22 = pxNewTCB->uxPriority; _23 = pxReadyTasksLists[_22].uxNumberOfItems; _24 = _23 + 1; pxReadyTasksLists[_22].uxNumberOfItems = _24; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT vPortExitCritical (); # DEBUG BEGIN_STMT xSchedulerRunning.10_25 = xSchedulerRunning; if (xSchedulerRunning.10_25 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxCurrentTCB.11_26 = pxCurrentTCB; _27 = pxCurrentTCB.11_26->uxPriority; _28 = pxNewTCB->uxPriority; if (_27 < _28) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _29 = 3758157060B; *_29 = 268435456; # DEBUG BEGIN_STMT __asm__ __volatile__("dsb" : : : "memory"); # DEBUG BEGIN_STMT __asm__ __volatile__("isb"); # DEBUG BEGIN_STMT : # DEBUG BEGIN_STMT return; } prvInitialiseNewTask (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint32_t ulStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask, struct TCB_t * pxNewTCB, const struct MemoryRegion_t * const xRegions) { UBaseType_t x; StackType_t * pxTopOfStack; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = pxNewTCB->pxStack; _2 = ulStackDepth * 4; memset (_1, 165, _2); # DEBUG BEGIN_STMT _3 = pxNewTCB->pxStack; _4 = ulStackDepth + 1073741823; _5 = _4 * 4; pxTopOfStack = _3 + _5; # DEBUG BEGIN_STMT pxTopOfStack.0_6 = (long unsigned int) pxTopOfStack; _7 = pxTopOfStack.0_6 & 4294967288; pxTopOfStack = (StackType_t *) _7; # DEBUG BEGIN_STMT pxTopOfStack.1_8 = (long unsigned int) pxTopOfStack; _9 = pxTopOfStack.1_8 & 7; if (_9 != 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (pcName != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT x = 0; goto ; [INV] : # DEBUG BEGIN_STMT _10 = pcName + x; _11 = *_10; pxNewTCB->pcTaskName[x] = _11; # DEBUG BEGIN_STMT _12 = pcName + x; _13 = *_12; if (_13 == 0) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT x = x + 1; : # DEBUG BEGIN_STMT if (x <= 9) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxNewTCB->pcTaskName[9] = 0; goto ; [INV] : # DEBUG BEGIN_STMT pxNewTCB->pcTaskName[0] = 0; : # DEBUG BEGIN_STMT if (uxPriority > 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT vPortRaiseBASEPRI (); : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT goto ; [INV] : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT if (uxPriority > 4) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT uxPriority = 4; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT pxNewTCB->uxPriority = uxPriority; # DEBUG BEGIN_STMT pxNewTCB->uxBasePriority = uxPriority; # DEBUG BEGIN_STMT pxNewTCB->uxMutexesHeld = 0; # DEBUG BEGIN_STMT _14 = &pxNewTCB->xStateListItem; vListInitialiseItem (_14); # DEBUG BEGIN_STMT _15 = &pxNewTCB->xEventListItem; vListInitialiseItem (_15); # DEBUG BEGIN_STMT pxNewTCB->xStateListItem.pvOwner = pxNewTCB; # DEBUG BEGIN_STMT _16 = 5 - uxPriority; pxNewTCB->xEventListItem.xItemValue = _16; # DEBUG BEGIN_STMT pxNewTCB->xEventListItem.pvOwner = pxNewTCB; # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _17 = &pxNewTCB->ulNotifiedValue[0]; memset (_17, 0, 4); # DEBUG BEGIN_STMT _18 = &pxNewTCB->ucNotifyState[0]; memset (_18, 0, 1); # DEBUG BEGIN_STMT pxNewTCB->ucDelayAborted = 0; # DEBUG BEGIN_STMT _19 = pxPortInitialiseStack (pxTopOfStack, pxTaskCode, pvParameters); pxNewTCB->pxTopOfStack = _19; # DEBUG BEGIN_STMT if (pxCreatedTask != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT *pxCreatedTask = pxNewTCB; : # DEBUG BEGIN_STMT return; } xTaskCreate (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint16_t usStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask) { StackType_t * pxStack; BaseType_t xReturn; struct TCB_t * pxNewTCB; BaseType_t D.7508; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT _1 = (unsigned int) usStackDepth; _2 = _1 * 4; pxStack = pvPortMalloc (_2); # DEBUG BEGIN_STMT if (pxStack != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxNewTCB = pvPortMalloc (88); # DEBUG BEGIN_STMT if (pxNewTCB != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT pxNewTCB->pxStack = pxStack; goto ; [INV] : # DEBUG BEGIN_STMT vPortFree (pxStack); goto ; [INV] : # DEBUG BEGIN_STMT pxNewTCB = 0B; : # DEBUG BEGIN_STMT if (pxNewTCB != 0B) goto ; [INV] else goto ; [INV] : # DEBUG BEGIN_STMT _3 = (long unsigned int) usStackDepth; prvInitialiseNewTask (pxTaskCode, pcName, _3, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0B); # DEBUG BEGIN_STMT prvAddNewTaskToReadyList (pxNewTCB); # DEBUG BEGIN_STMT xReturn = 1; goto ; [INV] : # DEBUG BEGIN_STMT xReturn = -1; : # DEBUG BEGIN_STMT D.7508 = xReturn; return D.7508; } __attribute__((always_inline)) vPortSetBASEPRI (uint32_t ulNewMaskValue) { : # DEBUG BEGIN_STMT __asm__ __volatile__(" msr basepri, %0 " : : "r" ulNewMaskValue : "memory"); return; } __attribute__((always_inline)) ulPortRaiseBASEPRI () { uint32_t ulNewBASEPRI; uint32_t ulOriginalBASEPRI; uint32_t D.7648; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT __asm__ __volatile__(" mrs %0, basepri mov %1, %2 msr basepri, %1 isb dsb " : "=r" ulOriginalBASEPRI, "=r" ulNewBASEPRI : "i" 16 : "memory"); # DEBUG BEGIN_STMT D.7648 = ulOriginalBASEPRI; return D.7648; } __attribute__((always_inline)) vPortRaiseBASEPRI () { uint32_t ulNewBASEPRI; : # DEBUG BEGIN_STMT # DEBUG BEGIN_STMT __asm__ __volatile__(" mov %0, %1 msr basepri, %0 isb dsb " : "=r" ulNewBASEPRI : "i" 16 : "memory"); return; }