diff --git a/tasks.c b/tasks.c index 78e8b1939..e1f4c5eb9 100644 --- a/tasks.c +++ b/tasks.c @@ -27,7 +27,7 @@ /* Verifast proof setup */ #ifdef VERIFAST #include "verifast_proof_defs.h" - #include "tasks.gh" + #include "task_predicates.h" #endif /* Standard includes. */ @@ -1359,6 +1359,9 @@ static void prvYieldForTask( TCB_t * pxTCB, { /* Store the stack location in the TCB. */ pxNewTCB->pxStack = pxStack; + //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); + //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); + //@ close TCB_p(pxNewTCB); } else { diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c index 97234d648..5984f1df7 100644 --- a/verification/verifast/preprocessed_files/tasks--pp.c +++ b/verification/verifast/preprocessed_files/tasks--pp.c @@ -43,18 +43,77 @@ // Delete keywords VeriFast canot parse (in some contexts) // # 30 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 -// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/tasks.gh" 1 +// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/task_predicates.h" 1 +// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/nathan/list_predicates.h" 1 + + + + +/* + * The code below has been taken from: + * pull request: + * https://github.com/FreeRTOS/FreeRTOS/pull/836 + * file: + * FreeRTOS/Test/VeriFast/include/proof/list.h + * + */ + +/*@ +predicate xLIST_ITEM( + struct xLIST_ITEM *n, + TickType_t xItemValue, + struct xLIST_ITEM *pxNext, + struct xLIST_ITEM *pxPrevious, + struct xLIST *pxContainer;) = + n->xItemValue |-> xItemValue &*& + n->pxNext |-> pxNext &*& + n->pxPrevious |-> pxPrevious &*& + n->pvOwner |-> _ &*& + n->pxContainer |-> pxContainer; +@*/ +// # 6 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/task_predicates.h" 2 + /*@ - -predicate TCB(TCB_t * tcb) = +// This predicate represents the memory corresponding to an +// instance of type `TCB_t` aka `tskTaskControlBlock`. +predicate TCB_p(TCB_t * tcb) = malloc_block_tskTaskControlBlock(tcb) &*& - tcb->pxStack |-> ?stack; + tcb->pxTopOfStack |-> _ &*& + xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*& + struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*& + xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*& + struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& + + tcb->uxPriority |-> _ &*& + tcb->pxStack |-> _ &*& + tcb->xTaskRunState |-> _ &*& + tcb->xIsIdle |-> _ &*& + + // pcTaskName + chars_(tcb->pcTaskName, 16, _) &*& + + tcb->uxCriticalNesting |-> _ &*& + tcb->uxTCBNumber |-> _ &*& + tcb->uxTaskNumber |-> _ &*& + tcb->uxBasePriority |-> _ &*& + tcb->uxMutexesHeld |-> _ &*& + + // void * pvThreadLocalStoragePointers[ 5 ]; + pointers_(tcb->pvThreadLocalStoragePointers, _, _) &*& + + integers__(tcb->ulNotifiedValue, _, _, _, _) &*& + + uchars_(tcb->ucNotifyState, 1, _) &*& + + tcb->ucDelayAborted |-> _; + + @*/ // # 31 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 @@ -10662,6 +10721,9 @@ static void prvYieldForTask( TCB_t * pxTCB, { /* Store the stack location in the TCB. */ pxNewTCB->pxStack = pxStack; + //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); + //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); + //@ close TCB_p(pxNewTCB); } else { @@ -10679,9 +10741,9 @@ static void prvYieldForTask( TCB_t * pxTCB, if( pxNewTCB != 0 ) { -// # 1387 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1390 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" prvInitialiseNewTask( pxTaskCode, pcName, ( uint32_t ) usStackDepth, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0 ); -// # 1396 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1399 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" prvAddNewTaskToReadyList( pxNewTCB ); xReturn = ( ( ( BaseType_t ) 1 ) ); } @@ -10711,7 +10773,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, { StackType_t * pxTopOfStack; UBaseType_t x; -// # 1441 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1444 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Avoid dependency on memset() if it is not required. */ { @@ -10730,10 +10792,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, pxTopOfStack = ( StackType_t * ) ( ( ( uint32_t ) pxTopOfStack ) & ( ~( ( uint32_t ) ( 0x0007 ) ) ) ); /*lint !e923 !e9033 !e9078 MISRA exception. Avoiding casts between pointers and integers is not practical. Size differences accounted for using portPOINTER_SIZE_TYPE type. Checked by assert(). */ /* Check the alignment of the calculated top of stack is correct. */ - (__builtin_expect(!(( ( ( uint32_t ) pxTopOfStack & ( uint32_t ) ( 0x0007 ) ) == 0UL )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1459, "( ( ( uint32_t ) pxTopOfStack & ( uint32_t ) ( 0x0007 ) ) == 0UL )") : (void)0); -// # 1468 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" + (__builtin_expect(!(( ( ( uint32_t ) pxTopOfStack & ( uint32_t ) ( 0x0007 ) ) == 0UL )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1462, "( ( ( uint32_t ) pxTopOfStack & ( uint32_t ) ( 0x0007 ) ) == 0UL )") : (void)0); +// # 1471 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } -// # 1482 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1485 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Store the task name in the TCB. */ if( pcName != 0 ) { @@ -10799,7 +10861,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, { pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U; } -// # 1566 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1569 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* Avoid compiler warning about unreferenced parameter. */ ( void ) xRegions; @@ -10817,21 +10879,21 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, memset( ( void * ) &( pxNewTCB->ulNotifiedValue[ 0 ] ), 0x00, sizeof( pxNewTCB->ulNotifiedValue ) ); memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) ); } -// # 1595 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1598 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { pxNewTCB->ucDelayAborted = ( ( BaseType_t ) 0 ); } -// # 1613 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1616 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Initialize the TCB stack to look as if the task was already running, * but had been interrupted by the scheduler. The return address is set * to the start of the task function. Once the stack has been initialised * the top of stack variable is updated. */ -// # 1641 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1644 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* If the port has capability to detect stack overflow, * pass the stack end address to the stack initialization * function as well. */ -// # 1658 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1661 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters ); } @@ -11040,7 +11102,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) if( xTaskRunningOnCore == xCoreID ) { - (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1866, "uxSchedulerSuspended == 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1869, "uxSchedulerSuspended == 0") : (void)0); vTaskYieldWithinAPI(); } else @@ -11063,12 +11125,12 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) TickType_t xTimeToWake; BaseType_t xAlreadyYielded, xShouldDelay = ( ( BaseType_t ) 0 ); - (__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1889, "pxPreviousWakeTime") : (void)0); - (__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1890, "( xTimeIncrement > 0U )") : (void)0); + (__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1892, "pxPreviousWakeTime") : (void)0); + (__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1893, "( xTimeIncrement > 0U )") : (void)0); vTaskSuspendAll(); { - (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1894, "uxSchedulerSuspended == 1") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1897, "uxSchedulerSuspended == 1") : (void)0); /* Minor optimisation. The tick count cannot change in this * block. */ @@ -11154,7 +11216,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) { vTaskSuspendAll(); { - (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1980, "uxSchedulerSuspended == 1") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1983, "uxSchedulerSuspended == 1") : (void)0); ; /* A task that is removed from the event list while the @@ -11208,7 +11270,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) const TCB_t * const pxTCB = xTask; - (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2034, "pxTCB") : (void)0); + (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2037, "pxTCB") : (void)0); vTaskEnterCritical(); { @@ -11384,7 +11446,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) BaseType_t xYieldForTask = ( ( BaseType_t ) 0 ); BaseType_t xCoreID; - (__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2210, "( uxNewPriority < 32 )") : (void)0); + (__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2213, "( uxNewPriority < 32 )") : (void)0); /* Ensure the new priority is valid. */ if( uxNewPriority >= ( UBaseType_t ) 32 ) @@ -11538,13 +11600,13 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) /*-----------------------------------------------------------*/ -// # 2398 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2401 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 2421 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2424 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 2439 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2442 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 2467 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2470 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -11621,7 +11683,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) if( xTaskRunningOnCore == 0 ) { /* The current task has just been suspended. */ - (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2543, "uxSchedulerSuspended == 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2546, "uxSchedulerSuspended == 0") : (void)0); vTaskYieldWithinAPI(); } else @@ -11635,7 +11697,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) { vTaskExitCritical(); - (__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2557, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0); + (__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2560, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0); /* The scheduler is not running, but the task that was pointed * to by pxCurrentTCB has just been suspended and pxCurrentTCB @@ -11682,7 +11744,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) /* Accesses xPendingReadyList so must be called from a critical section. */ /* It does not make sense to check if the calling task is suspended. */ - (__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2604, "xTask") : (void)0); + (__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2607, "xTask") : (void)0); /* Is the task being resumed actually in the suspended list? */ if( ( ( ( &( pxTCB->xStateListItem ) )->pxContainer == ( &xSuspendedTaskList ) ) ? ( ( ( BaseType_t ) 1 ) ) : ( ( ( BaseType_t ) 0 ) ) ) != ( ( BaseType_t ) 0 ) ) @@ -11731,7 +11793,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) /* It does not make sense to resume the calling task. */ - (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2653, "xTaskToResume") : (void)0); + (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2656, "xTaskToResume") : (void)0); /* The parameter cannot be NULL as it is impossible to resume the * currently executing task. It is also impossible to resume a task @@ -11790,7 +11852,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) UBaseType_t uxSavedInterruptStatus; - (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2712, "xTaskToResume") : (void)0); + (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2715, "xTaskToResume") : (void)0); /* RTOS ports that support interrupt nesting have the concept of a * maximum system call (or maximum API call) interrupt priority. @@ -11911,7 +11973,7 @@ static BaseType_t prvCreateIdleTasks( void ) { ; } -// # 2880 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2883 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { if( xCoreID == 0 ) { @@ -11923,7 +11985,7 @@ static BaseType_t prvCreateIdleTasks( void ) ( ( UBaseType_t ) 0x00 ), /* In effect ( tskIDLE_PRIORITY | portPRIVILEGE_BIT ), but tskIDLE_PRIORITY is zero. */ &xIdleTaskHandle[ xCoreID ] ); /*lint !e961 MISRA exception, justified as it is not a redundant explicit cast to all supported compilers. */ } -// # 2903 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2906 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } @@ -11960,7 +12022,7 @@ void vTaskStartScheduler( void ) * so interrupts will automatically get re-enabled when the first task * starts to run. */ assert_fct(false); -// # 2953 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2956 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL; xSchedulerRunning = ( ( BaseType_t ) 1 ); xTickCount = ( TickType_t ) 0; @@ -11992,7 +12054,7 @@ void vTaskStartScheduler( void ) /* This line will only be reached if the kernel could not be started, * because there was not enough FreeRTOS heap to create the idle task * or the timer task. */ - (__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2984, "xReturn != ( -1 )") : (void)0); + (__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2987, "xReturn != ( -1 )") : (void)0); } /* Prevent compiler warnings if INCLUDE_xTaskGetIdleTaskHandle is set to 0, @@ -12057,7 +12119,7 @@ void vTaskSuspendAll( void ) } } /*----------------------------------------------------------*/ -// # 3111 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3114 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ BaseType_t xTaskResumeAll( void ) @@ -12080,7 +12142,7 @@ BaseType_t xTaskResumeAll( void ) /* If uxSchedulerSuspended is zero then this function does not match a * previous call to vTaskSuspendAll(). */ - (__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3133, "uxSchedulerSuspended") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3136, "uxSchedulerSuspended") : (void)0); --uxSchedulerSuspended; vPortRecursiveLock(1, spin_lock_instance(15), ( ( BaseType_t ) 0 )); @@ -12238,7 +12300,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char /* If null is passed in here then the name of the calling task is being * queried. */ pxTCB = ( ( ( xTaskToQuery ) == 0 ) ? xTaskGetCurrentTaskHandle() : ( xTaskToQuery ) ); - (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3291, "pxTCB") : (void)0); + (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3294, "pxTCB") : (void)0); return &( pxTCB->pcTaskName[ 0 ] ); } /*-----------------------------------------------------------*/ @@ -12331,7 +12393,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char TCB_t * pxTCB; /* Task names will be truncated to configMAX_TASK_NAME_LEN - 1 bytes. */ - (__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3384, "strlen( pcNameToQuery ) < 16") : (void)0); + (__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3387, "strlen( pcNameToQuery ) < 16") : (void)0); vTaskSuspendAll(); { @@ -12427,7 +12489,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char * each task in the Suspended state. */ uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended ); } -// # 3494 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3497 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { if( pulTotalRunTime != 0 ) { @@ -12455,7 +12517,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char { /* If xTaskGetIdleTaskHandle() is called before the scheduler has been * started, then xIdleTaskHandle will be NULL. */ - (__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3521, "( xIdleTaskHandle != 0 )") : (void)0); + (__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3524, "( xIdleTaskHandle != 0 )") : (void)0); return &( xIdleTaskHandle[ 0 ] ); } @@ -12466,7 +12528,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char * This is to ensure vTaskStepTick() is available when user defined low power mode * implementations require configUSE_TICKLESS_IDLE to be set to a value other than * 1. */ -// # 3545 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3548 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp ) @@ -12475,7 +12537,7 @@ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp ) /* Must not be called with the scheduler suspended as the implementation * relies on xPendedTicks being wound down to 0 in xTaskResumeAll(). */ - (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3553, "uxSchedulerSuspended == 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3556, "uxSchedulerSuspended == 0") : (void)0); /* Use xPendedTicks to mimic xTicksToCatchUp number of ticks occurring when * the scheduler is suspended so the ticks are executed in xTaskResumeAll(). */ @@ -12494,7 +12556,7 @@ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp ) TCB_t * pxTCB = xTask; BaseType_t xReturn; - (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3572, "pxTCB") : (void)0); + (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3575, "pxTCB") : (void)0); vTaskSuspendAll(); { @@ -12593,7 +12655,7 @@ BaseType_t xTaskIncrementTick( void ) if( xConstTickCount == ( TickType_t ) 0U ) /*lint !e774 'if' does not always evaluate to false as it is looking for an overflow. */ { - { List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3671, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); }; + { List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3674, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( BaseType_t ) 1 ) : ( ( BaseType_t ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); }; } else { @@ -12776,13 +12838,13 @@ BaseType_t xTaskIncrementTick( void ) return xSwitchRequired; } /*-----------------------------------------------------------*/ -// # 3883 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3886 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 3907 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3910 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 3932 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3935 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 3965 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3968 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ void vTaskSwitchContext( BaseType_t xCoreID ) @@ -12800,7 +12862,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) { /* vTaskSwitchContext() must never be called from within a critical section. * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */ - (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3982, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0); + (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3985, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0); if( uxSchedulerSuspended != ( UBaseType_t ) ( ( BaseType_t ) 0 ) ) { @@ -12812,7 +12874,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) { xYieldPendings[ xCoreID ] = ( ( BaseType_t ) 0 ); ; -// # 4023 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4026 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Check for stack overflow, if configured. */ { const uint32_t * const pulStack = ( uint32_t * ) xTaskGetCurrentTaskHandle()->pxStack; const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; if( ( pulStack[ 0 ] != ulCheckValue ) || ( pulStack[ 1 ] != ulCheckValue ) || ( pulStack[ 2 ] != ulCheckValue ) || ( pulStack[ 3 ] != ulCheckValue ) ) { vApplicationStackOverflowHook( ( TaskHandle_t ) xTaskGetCurrentTaskHandle(), xTaskGetCurrentTaskHandle()->pcTaskName ); } }; @@ -12829,7 +12891,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) ; /* After the new task is switched in, update the global errno. */ -// # 4057 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4060 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } vPortRecursiveLock(0, spin_lock_instance(14), ( ( BaseType_t ) 0 )); @@ -12840,7 +12902,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) void vTaskPlaceOnEventList( List_t * const pxEventList, const TickType_t xTicksToWait ) { - (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4067, "pxEventList") : (void)0); + (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4070, "pxEventList") : (void)0); /* THIS FUNCTION MUST BE CALLED WITH EITHER INTERRUPTS DISABLED OR THE * SCHEDULER SUSPENDED AND THE QUEUE BEING ACCESSED LOCKED. */ @@ -12859,11 +12921,11 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList, const TickType_t xItemValue, const TickType_t xTicksToWait ) { - (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4086, "pxEventList") : (void)0); + (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4089, "pxEventList") : (void)0); /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. It is used by * the event groups implementation. */ - (__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4090, "uxSchedulerSuspended != 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4093, "uxSchedulerSuspended != 0") : (void)0); /* Store the item value in the event list item. It is safe to access the * event list item here as interrupts won't access the event list item of a @@ -12887,7 +12949,7 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely ) { - (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4114, "pxEventList") : (void)0); + (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4117, "pxEventList") : (void)0); /* This function should not be called by application code hence the * 'Restricted' in its name. It is not part of the public API. It is @@ -12935,14 +12997,14 @@ BaseType_t xTaskRemoveFromEventList( const List_t * const pxEventList ) * This function assumes that a check has already been made to ensure that * pxEventList is not empty. */ pxUnblockedTCB = ( ( &( ( pxEventList )->xListEnd ) )->pxNext->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too. Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */ - (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4162, "pxUnblockedTCB") : (void)0); + (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4165, "pxUnblockedTCB") : (void)0); ( void ) uxListRemove( &( pxUnblockedTCB->xEventListItem ) ); if( uxSchedulerSuspended == ( UBaseType_t ) ( ( BaseType_t ) 0 ) ) { ( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) ); ; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ; -// # 4183 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4186 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } else { @@ -12972,7 +13034,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem, /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. It is used by * the event flags implementation. */ - (__builtin_expect(!(uxSchedulerSuspended != ( ( BaseType_t ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4212, "uxSchedulerSuspended != ( ( BaseType_t ) 0 )") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended != ( ( BaseType_t ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4215, "uxSchedulerSuspended != ( ( BaseType_t ) 0 )") : (void)0); /* Store the new item value in the event list. */ ( ( pxEventListItem )->xItemValue = ( xItemValue | 0x80000000UL ) ); @@ -12980,9 +13042,9 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem, /* Remove the event list form the event flag. Interrupts do not access * event flags. */ pxUnblockedTCB = ( ( pxEventListItem )->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too. Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */ - (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4220, "pxUnblockedTCB") : (void)0); + (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4223, "pxUnblockedTCB") : (void)0); ( void ) uxListRemove( pxEventListItem ); -// # 4237 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4240 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Remove the task from the delayed list and add it to the ready list. The * scheduler is suspended so interrupts will not be accessing the ready * lists. */ @@ -13001,7 +13063,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem, void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut ) { - (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4255, "pxTimeOut") : (void)0); + (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4258, "pxTimeOut") : (void)0); vTaskEnterCritical(); { pxTimeOut->xOverflowCount = xNumOfOverflows; @@ -13024,8 +13086,8 @@ BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, { BaseType_t xReturn; - (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4278, "pxTimeOut") : (void)0); - (__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4279, "pxTicksToWait") : (void)0); + (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4281, "pxTimeOut") : (void)0); + (__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4282, "pxTicksToWait") : (void)0); vTaskEnterCritical(); { @@ -13147,7 +13209,7 @@ void vTaskMissedYield( void ) * * @todo additional conditional compiles to remove this function. */ -// # 4461 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4464 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* * ----------------------------------------------------------- * The Idle task. @@ -13177,7 +13239,7 @@ static void prvIdleTask( void * pvParameters ) /* See if any tasks have deleted themselves - if so then the idle task * is responsible for freeing the deleted task's TCB and stack. */ prvCheckTasksWaitingTermination(); -// # 4502 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4505 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* When using preemption tasks of equal priority will be * timesliced. If a task that is sharing the idle priority is ready @@ -13198,16 +13260,16 @@ static void prvIdleTask( void * pvParameters ) ; } } -// # 4538 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4541 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* This conditional compilation should use inequality to 0, not equality * to 1. This is to ensure portSUPPRESS_TICKS_AND_SLEEP() is called when * user defined low power mode implementations require * configUSE_TICKLESS_IDLE to be set to a value other than 1. */ -// # 4603 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4606 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } /*-----------------------------------------------------------*/ -// # 4653 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4656 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -13221,7 +13283,7 @@ static void prvIdleTask( void * pvParameters ) if( xIndex < 5 ) { pxTCB = ( ( ( xTaskToSet ) == 0 ) ? xTaskGetCurrentTaskHandle() : ( xTaskToSet ) ); - (__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4666, "pxTCB != 0") : (void)0); + (__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4669, "pxTCB != 0") : (void)0); pxTCB->pvThreadLocalStoragePointers[ xIndex ] = pvValue; } } @@ -13252,7 +13314,7 @@ static void prvIdleTask( void * pvParameters ) /*-----------------------------------------------------------*/ -// # 4713 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4716 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvInitialiseTaskLists( void ) @@ -13354,7 +13416,7 @@ static void prvCheckTasksWaitingTermination( void ) { pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority; } -// # 4825 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4828 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { pxTaskStatus->ulRunTimeCounter = 0; } @@ -13485,7 +13547,7 @@ static void prvCheckTasksWaitingTermination( void ) /*-----------------------------------------------------------*/ -// # 4994 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4997 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -13542,7 +13604,7 @@ static void prvCheckTasksWaitingTermination( void ) free( (void*) pxTCB->pxStack); free( (void*) pxTCB); } -// # 5077 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5080 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } @@ -13747,8 +13809,8 @@ static void prvResetNextTaskUnblockTime( void ) * If the mutex is held by a task then it cannot be given from an * interrupt, and if a mutex is given by the holding task then it must * be the running state task. */ - (__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5281, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0); - (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5282, "pxTCB->uxMutexesHeld") : (void)0); + (__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5284, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0); + (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5285, "pxTCB->uxMutexesHeld") : (void)0); ( pxTCB->uxMutexesHeld )--; /* Has the holder of the mutex inherited the priority of another @@ -13834,7 +13896,7 @@ static void prvResetNextTaskUnblockTime( void ) { /* If pxMutexHolder is not NULL then the holder must hold at least * one mutex. */ - (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5368, "pxTCB->uxMutexesHeld") : (void)0); + (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5371, "pxTCB->uxMutexesHeld") : (void)0); /* Determine the priority to which the priority of the task that * holds the mutex should be set. This will be the greater of the @@ -13861,7 +13923,7 @@ static void prvResetNextTaskUnblockTime( void ) /* If a task has timed out because it already holds the * mutex it was trying to obtain then it cannot of inherited * its own priority. */ - (__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5395, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0); + (__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5398, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0); /* Disinherit the priority, remembering the previous * priority to facilitate determining the subject task's @@ -13992,7 +14054,7 @@ void vTaskYieldWithinAPI( void ) { /* If pxCurrentTCB->uxCriticalNesting is zero then this function * does not match a previous call to vTaskEnterCritical(). */ - (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5526, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0); + (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5529, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0); if( xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U ) { @@ -14042,11 +14104,11 @@ void vTaskYieldWithinAPI( void ) /*-----------------------------------------------------------*/ -// # 5602 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5605 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 5708 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5711 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ -// # 5835 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5838 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ TickType_t uxTaskResetEventItemValue( void ) @@ -14088,7 +14150,7 @@ TickType_t uxTaskResetEventItemValue( void ) { uint32_t ulReturn; - (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5876, "uxIndexToWait < 1") : (void)0); + (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5879, "uxIndexToWait < 1") : (void)0); vTaskEnterCritical(); { @@ -14162,7 +14224,7 @@ TickType_t uxTaskResetEventItemValue( void ) { BaseType_t xReturn; - (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5950, "uxIndexToWait < 1") : (void)0); + (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5953, "uxIndexToWait < 1") : (void)0); vTaskEnterCritical(); { @@ -14250,8 +14312,8 @@ TickType_t uxTaskResetEventItemValue( void ) BaseType_t xReturn = ( ( ( BaseType_t ) 1 ) ); uint8_t ucOriginalNotifyState; - (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6038, "uxIndexToNotify < 1") : (void)0); - (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6039, "xTaskToNotify") : (void)0); + (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6041, "uxIndexToNotify < 1") : (void)0); + (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6042, "xTaskToNotify") : (void)0); pxTCB = xTaskToNotify; vTaskEnterCritical(); @@ -14304,7 +14366,7 @@ TickType_t uxTaskResetEventItemValue( void ) /* Should not get here if all enums are handled. * Artificially force an assert by testing a value the * compiler can't assume is const. */ - (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6092, "xTickCount == ( TickType_t ) 0") : (void)0); + (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6095, "xTickCount == ( TickType_t ) 0") : (void)0); break; } @@ -14319,8 +14381,8 @@ TickType_t uxTaskResetEventItemValue( void ) ; { if( ( ( pxTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxTCB )->uxPriority ] ), &( ( pxTCB )->xStateListItem ) ); ; /* The task should not have been on an event list. */ - (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6107, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); -// # 6126 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" + (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6110, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); +// # 6129 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { prvYieldForTask( pxTCB, ( ( BaseType_t ) 0 ) ); } @@ -14353,8 +14415,8 @@ TickType_t uxTaskResetEventItemValue( void ) BaseType_t xReturn = ( ( ( BaseType_t ) 1 ) ); UBaseType_t uxSavedInterruptStatus; - (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6158, "xTaskToNotify") : (void)0); - (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6159, "uxIndexToNotify < 1") : (void)0); + (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6161, "xTaskToNotify") : (void)0); + (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6162, "uxIndexToNotify < 1") : (void)0); /* RTOS ports that support interrupt nesting have the concept of a * maximum system call (or maximum API call) interrupt priority. @@ -14425,7 +14487,7 @@ TickType_t uxTaskResetEventItemValue( void ) /* Should not get here if all enums are handled. * Artificially force an assert by testing a value the * compiler can't assume is const. */ - (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6230, "xTickCount == ( TickType_t ) 0") : (void)0); + (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6233, "xTickCount == ( TickType_t ) 0") : (void)0); break; } @@ -14436,7 +14498,7 @@ TickType_t uxTaskResetEventItemValue( void ) if( ucOriginalNotifyState == ( ( uint8_t ) 1 ) ) { /* The task should not have been on an event list. */ - (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6241, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); + (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6244, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); if( uxSchedulerSuspended == ( UBaseType_t ) ( ( BaseType_t ) 0 ) ) { @@ -14481,8 +14543,8 @@ TickType_t uxTaskResetEventItemValue( void ) uint8_t ucOriginalNotifyState; UBaseType_t uxSavedInterruptStatus; - (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6286, "xTaskToNotify") : (void)0); - (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6287, "uxIndexToNotify < 1") : (void)0); + (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6289, "xTaskToNotify") : (void)0); + (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6290, "uxIndexToNotify < 1") : (void)0); /* RTOS ports that support interrupt nesting have the concept of a * maximum system call (or maximum API call) interrupt priority. @@ -14520,7 +14582,7 @@ TickType_t uxTaskResetEventItemValue( void ) if( ucOriginalNotifyState == ( ( uint8_t ) 1 ) ) { /* The task should not have been on an event list. */ - (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6325, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); + (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6328, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); if( uxSchedulerSuspended == ( UBaseType_t ) ( ( BaseType_t ) 0 ) ) { @@ -14561,7 +14623,7 @@ TickType_t uxTaskResetEventItemValue( void ) TCB_t * pxTCB; BaseType_t xReturn; - (__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6366, "uxIndexToClear < 1") : (void)0); + (__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6369, "uxIndexToClear < 1") : (void)0); /* If null is passed in here then it is the calling task that is having * its notification state cleared. */ @@ -14614,7 +14676,7 @@ TickType_t uxTaskResetEventItemValue( void ) /*-----------------------------------------------------------*/ -// # 6435 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6438 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, @@ -14690,7 +14752,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, } } } -// # 6547 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6550 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } /* Code below here allows additional code to be inserted into this source file, diff --git a/verification/verifast/proof/nathan/README.md b/verification/verifast/proof/nathan/README.md new file mode 100644 index 000000000..d8b83cacb --- /dev/null +++ b/verification/verifast/proof/nathan/README.md @@ -0,0 +1,3 @@ +This directory contains proof artifacts written by Nathan Chong. +See the following pull request: +https://github.com/FreeRTOS/FreeRTOS/pull/836 diff --git a/verification/verifast/proof/nathan/list_predicates.h b/verification/verifast/proof/nathan/list_predicates.h new file mode 100644 index 000000000..7731a0a66 --- /dev/null +++ b/verification/verifast/proof/nathan/list_predicates.h @@ -0,0 +1,28 @@ +#ifndef LIST_PREDICATES_H + +#define LIST_PREDICATES_H + +/* + * The code below has been taken from: + * pull request: + * https://github.com/FreeRTOS/FreeRTOS/pull/836 + * file: + * FreeRTOS/Test/VeriFast/include/proof/list.h + * + */ + +/*@ +predicate xLIST_ITEM( + struct xLIST_ITEM *n, + TickType_t xItemValue, + struct xLIST_ITEM *pxNext, + struct xLIST_ITEM *pxPrevious, + struct xLIST *pxContainer;) = + n->xItemValue |-> xItemValue &*& + n->pxNext |-> pxNext &*& + n->pxPrevious |-> pxPrevious &*& + n->pvOwner |-> _ &*& + n->pxContainer |-> pxContainer; +@*/ + +#endif /* LIST_PREDICATES_H */ \ No newline at end of file diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h new file mode 100644 index 000000000..308866bbe --- /dev/null +++ b/verification/verifast/proof/task_predicates.h @@ -0,0 +1,46 @@ +#ifndef TASKS_GH + +#define TASKS_GH + +#include "nathan/list_predicates.h" + + +/*@ +// This predicate represents the memory corresponding to an +// instance of type `TCB_t` aka `tskTaskControlBlock`. +predicate TCB_p(TCB_t * tcb) = + malloc_block_tskTaskControlBlock(tcb) &*& + tcb->pxTopOfStack |-> _ &*& + + xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*& + struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*& + xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*& + struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& + + tcb->uxPriority |-> _ &*& + tcb->pxStack |-> _ &*& + tcb->xTaskRunState |-> _ &*& + tcb->xIsIdle |-> _ &*& + + // pcTaskName + chars_(tcb->pcTaskName, 16, _) &*& + + tcb->uxCriticalNesting |-> _ &*& + tcb->uxTCBNumber |-> _ &*& + tcb->uxTaskNumber |-> _ &*& + tcb->uxBasePriority |-> _ &*& + tcb->uxMutexesHeld |-> _ &*& + + // void * pvThreadLocalStoragePointers[ 5 ]; + pointers_(tcb->pvThreadLocalStoragePointers, _, _) &*& + + integers__(tcb->ulNotifiedValue, _, _, _, _) &*& + + uchars_(tcb->ucNotifyState, 1, _) &*& + + tcb->ucDelayAborted |-> _; + + +@*/ + +#endif /* TASKS_GH */ \ No newline at end of file diff --git a/verification/verifast/proof/tasks.gh b/verification/verifast/proof/tasks.gh deleted file mode 100644 index 211096f61..000000000 --- a/verification/verifast/proof/tasks.gh +++ /dev/null @@ -1,14 +0,0 @@ -#ifndef TASKS_GH - -#define TASKS_GH - - -/*@ - -predicate TCB(TCB_t * tcb) = - malloc_block_tskTaskControlBlock(tcb) &*& - tcb->pxStack |-> ?stack; - -@*/ - -#endif /* TASKS_GH */ \ No newline at end of file