diff --git a/tasks.c b/tasks.c index 06ac7c498..b5d84e206 100644 --- a/tasks.c +++ b/tasks.c @@ -47,6 +47,7 @@ */ #ifdef VERIFAST #include "verifast_proof_defs.h" + #include "stack_predicates.h" #include "task_predicates.h" #include "verifast_RP2040_axioms.h" #include "verifast_prelude_extended.h" diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c index ca4ec1659..16afe1f46 100644 --- a/verification/verifast/preprocessed_files/tasks--pp.c +++ b/verification/verifast/preprocessed_files/tasks--pp.c @@ -9941,6 +9941,61 @@ BaseType_t xTimerGenericCommandFromISR( TimerHandle_t xTimer, * type safe. Hence we define */ // # 50 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 +// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/stack_predicates.h" 1 + + + + +/*@ +// Represents a stack that grows down (cf. RP2040 stack) +predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) = + integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*& + ulStackDepth > 0 &*& + freeCells >= 0 &*& + pxTopOfStack == pxStack + freeCells -1 &*& + 0 <= freeCells &*& freeCells <= ulStackDepth; +// usedMem == pxStack - pxTopOfStack +// freeMem == ulStackDepth - usedMem + //freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*& +// usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack); +@*/ + +/*/@ +lemma void split_stack(StackType_t * pxStack, int offset) +requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*& + offset * sizeof(StackType_t) < ulStackDepth; +ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*& + integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ; +{ + open stack_p(_, _, _, _); + integers__split(pxStack, offset * sizeof(StackType_t) ); +} +@*/ + +/*@ +// TODO: Do we need this lemma or is it usually cleaner to split stack manually? +lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack) +requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*& + freeCells > 0; +ensures // free cells minus top cell + integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _) &*& + // top stack cell + integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*& + // used stack cells + integers_(pxStack + freeCells, sizeof(StackType_t), false, + ulStackDepth - freeCells, _) &*& + // stack contraints necessary to close `stack_p` again + ulStackDepth > 0 &*& + freeCells >= 0 &*& + pxTopOfStack == pxStack + freeCells -1 &*& + 0 <= freeCells &*& freeCells <= ulStackDepth; +{ + open stack_p(_, _, _, _); + integers__split(pxStack, freeCells-1); + open integers_(pxStack + (freeCells-1), _, _, _, _); +} +@*/ +// # 51 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/task_predicates.h" 1 @@ -10018,7 +10073,7 @@ predicate TCB_p(TCB_t * tcb, int stackSize) = @*/ -// # 51 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 +// # 52 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof_setup/verifast_RP2040_axioms.h" 1 @@ -10036,7 +10091,7 @@ lemma void ptr_range(t* ptr); requires true; ensures 0 <= (int) ptr &*& (int) ptr <= 4294967295; @*/ -// # 52 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 +// # 53 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/verifast_prelude_extended.h" 1 @@ -10089,7 +10144,7 @@ lemma_auto void integers___to_integers_(void *p); requires [?f]integers__(p, ?size, ?signed_, ?count, _); ensures [f]integers_(p, size, signed_, count, _); @*/ -// # 53 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 +// # 54 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof_setup/verifast_asm.h" 1 @@ -10115,7 +10170,7 @@ bool assert_fct(bool b) * VeriFast does not support embedding block statements that consist of * multiple elemts in expression contexts, e.g., `({e1; e2})`. */ -// # 54 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 +// # 55 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 // # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/snippets/rp2040_port_c_snippets.c" 1 /* @@ -10177,54 +10232,7 @@ static void vPortStartFirstTask( void ) ; */ static void prvTaskExitError( void ); -/*@ -// Represents a stack that grows down. -predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) = - integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*& - ulStackDepth > 0 &*& - freeCells >= 0 &*& - pxTopOfStack == pxStack + freeCells -1 &*& - 0 <= freeCells &*& freeCells <= ulStackDepth; -// usedMem == pxStack - pxTopOfStack -// freeMem == ulStackDepth - usedMem - //freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*& -// usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack); -@*/ -/*/@ -lemma void split_stack(StackType_t * pxStack, int offset) -requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*& - offset * sizeof(StackType_t) < ulStackDepth; -ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*& - integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ; -{ - open stack_p(_, _, _, _); - integers__split(pxStack, offset * sizeof(StackType_t) ); -} -@*/ - -/*@ -lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack) -requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*& - freeCells > 0; -ensures // free cells minus top cell - integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _) &*& - // top stack cell - integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*& - // used stack cells - integers_(pxStack + freeCells, sizeof(StackType_t), false, - ulStackDepth - freeCells, _) &*& - // stack contraints necessary to close `stack_p` again - ulStackDepth > 0 &*& - freeCells >= 0 &*& - pxTopOfStack == pxStack + freeCells -1 &*& - 0 <= freeCells &*& freeCells <= ulStackDepth; -{ - open stack_p(_, _, _, _); - integers__split(pxStack, freeCells-1); - open integers_(pxStack + (freeCells-1), _, _, _, _); -} -@*/ // ------------------------------------------------- @@ -10306,7 +10314,7 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, //@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth-16); return pxTopOfStack; } -// # 56 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 +// # 57 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2 /* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified @@ -10317,7 +10325,7 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, /* Set configUSE_STATS_FORMATTING_FUNCTIONS to 2 to include the stats formatting * functions but without including stdio.h here. */ -// # 84 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 85 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* Values that can be assigned to the ucNotifyState member of the TCB. */ @@ -10374,18 +10382,18 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, /* uxTopReadyPriority holds the priority of the highest priority ready * state task. */ -// # 148 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 149 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ /* Define away taskRESET_READY_PRIORITY() and portRESET_READY_PRIORITY() as * they are only required when a port optimised method of task selection is * being used. */ -// # 182 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 183 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ /* pxDelayedTaskList and pxOverflowDelayedTaskList are switched when the tick * count overflows. */ -// # 200 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 201 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ /* @@ -10440,7 +10448,7 @@ typedef BaseType_t TaskRunning_t; typedef struct tskTaskControlBlock /* The old naming convention is used to prevent breaking kernel aware debuggers. */ { volatile StackType_t * pxTopOfStack; /*< Points to the location of the last item placed on the tasks stack. THIS MUST BE THE FIRST MEMBER OF THE TCB STRUCT. */ -// # 263 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 264 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" ListItem_t xStateListItem; /*< The list that the state list item of a task is reference from denotes the state of that task (Ready, Blocked, Suspended ). */ ListItem_t xEventListItem; /*< Used to reference a task from an event list. */ UBaseType_t uxPriority; /*< The priority of the task. 0 is the lowest priority. */ @@ -10448,7 +10456,7 @@ typedef struct tskTaskControlBlock /* The old naming convention is used to preve volatile TaskRunning_t xTaskRunState; /*< Used to identify the core the task is running on, if any. */ BaseType_t xIsIdle; /*< Used to identify the idle tasks. */ char pcTaskName[ 16 ]; /*< Descriptive name given to the task when created. Facilitates debugging only. */ /*lint !e971 Unqualified char types are allowed for strings and single characters only. */ -// # 280 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 281 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" UBaseType_t uxCriticalNesting; /*< Holds the critical section nesting depth for ports that do not maintain their own count in the port layer. */ @@ -10468,7 +10476,7 @@ typedef struct tskTaskControlBlock /* The old naming convention is used to preve void * pvThreadLocalStoragePointers[ 5 ]; -// # 320 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 321 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" volatile uint32_t ulNotifiedValue[ 1 ]; volatile uint8_t ucNotifyState[ 1 ]; @@ -10559,7 +10567,7 @@ const volatile UBaseType_t uxTopUsedPriority = 32 - 1U; * must not be done by an ISR. Reads must be protected by either lock and may be done by * either an ISR or a task. */ static volatile UBaseType_t uxSchedulerSuspended = ( UBaseType_t ) ( ( char ) 0 ); -// # 420 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 421 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*lint -restore */ /*-----------------------------------------------------------*/ @@ -10712,7 +10720,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, * will exit the Blocked state. */ static void prvResetNextTaskUnblockTime( void ) ; -// # 584 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 585 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* * Called after a Task_t structure has been allocated either statically or * dynamically to fill in the structure's members. @@ -10744,9 +10752,9 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) ; /*-----------------------------------------------------------*/ -// # 634 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 635 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 717 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 718 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvYieldCore( BaseType_t xCoreID ) @@ -10788,8 +10796,8 @@ static void prvYieldForTask( TCB_t * pxTCB, /* THIS FUNCTION MUST BE CALLED FROM A CRITICAL SECTION */ - (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 758, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0); -// # 771 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" + (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 759, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0); +// # 772 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" xLowestPriority = ( BaseType_t ) pxTCB->uxPriority; if( xPreemptEqualPriority == ( ( char ) 0 ) ) @@ -10828,7 +10836,7 @@ static void prvYieldForTask( TCB_t * pxTCB, { ; } -// # 825 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 826 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } else { @@ -10841,7 +10849,7 @@ static void prvYieldForTask( TCB_t * pxTCB, prvYieldCore( xLowestPriorityCore ); xYieldCount++; } -// # 845 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 846 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } /*-----------------------------------------------------------*/ @@ -10852,10 +10860,10 @@ static void prvYieldForTask( TCB_t * pxTCB, UBaseType_t uxCurrentPriority = uxTopReadyPriority; BaseType_t xTaskScheduled = ( ( char ) 0 ); BaseType_t xDecrementTopPriority = ( ( char ) 1 ); -// # 863 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 864 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" while( xTaskScheduled == ( ( char ) 0 ) ) { -// # 877 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 878 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" if( ( ( ( &( pxReadyTasksLists[ uxCurrentPriority ] ) )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) == ( ( char ) 0 ) ) { @@ -10893,7 +10901,7 @@ static void prvYieldForTask( TCB_t * pxTCB, pxTCB = pxTaskItem->pvOwner; /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ -// # 930 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 931 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" if( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -1 ) ) { @@ -10914,7 +10922,7 @@ static void prvYieldForTask( TCB_t * pxTCB, } else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) { - (__builtin_expect(!(( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -2 ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 950, "( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -2 ) )") : (void)0); + (__builtin_expect(!(( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -2 ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 951, "( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -2 ) )") : (void)0); @@ -10958,21 +10966,21 @@ static void prvYieldForTask( TCB_t * pxTCB, return ( ( char ) 0 ); } - (__builtin_expect(!(( uxCurrentPriority > ( ( UBaseType_t ) 0U ) ) || ( xTaskScheduled == ( ( char ) 1 ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 994, "( uxCurrentPriority > ( ( UBaseType_t ) 0U ) ) || ( xTaskScheduled == ( ( char ) 1 ) )") : (void)0); + (__builtin_expect(!(( uxCurrentPriority > ( ( UBaseType_t ) 0U ) ) || ( xTaskScheduled == ( ( char ) 1 ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 995, "( uxCurrentPriority > ( ( UBaseType_t ) 0U ) ) || ( xTaskScheduled == ( ( char ) 1 ) )") : (void)0); uxCurrentPriority--; } - (__builtin_expect(!(( ( 0 <= pxCurrentTCBs[ xCoreID ]->xTaskRunState ) && ( pxCurrentTCBs[ xCoreID ]->xTaskRunState < 1 ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 998, "( ( 0 <= pxCurrentTCBs[ xCoreID ]->xTaskRunState ) && ( pxCurrentTCBs[ xCoreID ]->xTaskRunState < 1 ) )") : (void)0); -// # 1074 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" + (__builtin_expect(!(( ( 0 <= pxCurrentTCBs[ xCoreID ]->xTaskRunState ) && ( pxCurrentTCBs[ xCoreID ]->xTaskRunState < 1 ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 999, "( ( 0 <= pxCurrentTCBs[ xCoreID ]->xTaskRunState ) && ( pxCurrentTCBs[ xCoreID ]->xTaskRunState < 1 ) )") : (void)0); +// # 1075 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" return ( ( char ) 1 ); } -// # 1090 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1091 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 1168 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1169 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 1231 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1232 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 1297 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1298 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -10989,7 +10997,7 @@ static void prvYieldForTask( TCB_t * pxTCB, chars(pcName, 16, _); @*/ //@ ensures true; -// # 1326 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1327 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { TCB_t * pxNewTCB; BaseType_t xReturn; @@ -10997,7 +11005,7 @@ static void prvYieldForTask( TCB_t * pxTCB, /* If the stack grows down then allocate the stack then the TCB so the stack * does not grow into the TCB. Likewise if the stack grows up then allocate * the TCB then the stack. */ -// # 1356 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1357 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { StackType_t * pxStack; @@ -11033,9 +11041,9 @@ static void prvYieldForTask( TCB_t * pxTCB, if( pxNewTCB != 0 ) { -// # 1399 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1400 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" prvInitialiseNewTask( pxTaskCode, pcName, ( uint32_t ) usStackDepth, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0 ); -// # 1408 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1409 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" prvAddNewTaskToReadyList( pxNewTCB ); xReturn = ( ( ( char ) 1 ) ); } @@ -11073,7 +11081,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, { StackType_t * pxTopOfStack; UBaseType_t x; -// # 1462 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1463 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" //@ open TCB_p(_,_); /* Avoid dependency on memset() if it is not required. */ @@ -11120,9 +11128,9 @@ 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. */ -// # 1522 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1523 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } -// # 1536 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1537 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" //@ close TCB_p(pxNewTCB, stackSize); /* Store the task name in the TCB. */ @@ -11212,7 +11220,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, { pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U; } -// # 1644 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1645 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* Avoid compiler warning about unreferenced parameter. */ ( void ) xRegions; @@ -11239,7 +11247,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, //@ uchars__to_chars_(pxNewTCB->ucNotifyState); memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) ); } -// # 1682 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1683 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { /* Reason for rewrite: Assignment not type safe. */ @@ -11248,17 +11256,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, } -// # 1705 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1706 "/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. */ -// # 1733 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1734 "/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. */ -// # 1750 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 1751 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters ); } @@ -11469,7 +11477,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) if( xTaskRunningOnCore == xCoreID ) { - (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1960, "uxSchedulerSuspended == 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1961, "uxSchedulerSuspended == 0") : (void)0); vTaskYieldWithinAPI(); } else @@ -11492,12 +11500,12 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) TickType_t xTimeToWake; BaseType_t xAlreadyYielded, xShouldDelay = ( ( char ) 0 ); - (__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1983, "pxPreviousWakeTime") : (void)0); - (__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1984, "( xTimeIncrement > 0U )") : (void)0); + (__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1984, "pxPreviousWakeTime") : (void)0); + (__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1985, "( xTimeIncrement > 0U )") : (void)0); vTaskSuspendAll(); { - (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1988, "uxSchedulerSuspended == 1") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1989, "uxSchedulerSuspended == 1") : (void)0); /* Minor optimisation. The tick count cannot change in this * block. */ @@ -11583,7 +11591,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) { vTaskSuspendAll(); { - (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2074, "uxSchedulerSuspended == 1") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2075, "uxSchedulerSuspended == 1") : (void)0); ; /* A task that is removed from the event list while the @@ -11637,7 +11645,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) const TCB_t * const pxTCB = xTask; - (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2128, "pxTCB") : (void)0); + (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2129, "pxTCB") : (void)0); vTaskEnterCritical(); { @@ -11813,7 +11821,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) BaseType_t xYieldForTask = ( ( char ) 0 ); BaseType_t xCoreID; - (__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2304, "( uxNewPriority < 32 )") : (void)0); + (__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2305, "( uxNewPriority < 32 )") : (void)0); /* Ensure the new priority is valid. */ if( uxNewPriority >= ( UBaseType_t ) 32 ) @@ -11967,13 +11975,13 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) /*-----------------------------------------------------------*/ -// # 2492 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2493 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 2515 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2516 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 2533 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2534 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 2561 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2562 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -12050,7 +12058,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", 2637, "uxSchedulerSuspended == 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2638, "uxSchedulerSuspended == 0") : (void)0); vTaskYieldWithinAPI(); } else @@ -12064,7 +12072,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) { vTaskExitCritical(); - (__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2651, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0); + (__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2652, "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 @@ -12111,7 +12119,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", 2698, "xTask") : (void)0); + (__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2699, "xTask") : (void)0); /* Is the task being resumed actually in the suspended list? */ if( ( ( ( &( pxTCB->xStateListItem ) )->pxContainer == ( &xSuspendedTaskList ) ) ? ( ( ( char ) 1 ) ) : ( ( ( char ) 0 ) ) ) != ( ( char ) 0 ) ) @@ -12160,7 +12168,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", 2747, "xTaskToResume") : (void)0); + (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2748, "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 @@ -12219,7 +12227,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) UBaseType_t uxSavedInterruptStatus; - (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2806, "xTaskToResume") : (void)0); + (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2807, "xTaskToResume") : (void)0); /* RTOS ports that support interrupt nesting have the concept of a * maximum system call (or maximum API call) interrupt priority. @@ -12340,7 +12348,7 @@ static BaseType_t prvCreateIdleTasks( void ) { ; } -// # 2974 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2975 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { if( xCoreID == 0 ) { @@ -12352,7 +12360,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. */ } -// # 2997 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 2998 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } @@ -12389,7 +12397,7 @@ void vTaskStartScheduler( void ) * so interrupts will automatically get re-enabled when the first task * starts to run. */ assert_fct(false); -// # 3047 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3048 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL; xSchedulerRunning = ( ( char ) 1 ); xTickCount = ( TickType_t ) 0; @@ -12421,7 +12429,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", 3078, "xReturn != ( -1 )") : (void)0); + (__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3079, "xReturn != ( -1 )") : (void)0); } /* Prevent compiler warnings if INCLUDE_xTaskGetIdleTaskHandle is set to 0, @@ -12486,7 +12494,7 @@ void vTaskSuspendAll( void ) } } /*----------------------------------------------------------*/ -// # 3205 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3206 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ BaseType_t xTaskResumeAll( void ) @@ -12509,7 +12517,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", 3227, "uxSchedulerSuspended") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3228, "uxSchedulerSuspended") : (void)0); --uxSchedulerSuspended; vPortRecursiveLock(1, spin_lock_instance(15), ( ( char ) 0 )); @@ -12667,7 +12675,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", 3385, "pxTCB") : (void)0); + (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3386, "pxTCB") : (void)0); return &( pxTCB->pcTaskName[ 0 ] ); } /*-----------------------------------------------------------*/ @@ -12760,7 +12768,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", 3478, "strlen( pcNameToQuery ) < 16") : (void)0); + (__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3479, "strlen( pcNameToQuery ) < 16") : (void)0); vTaskSuspendAll(); { @@ -12856,7 +12864,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char * each task in the Suspended state. */ uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended ); } -// # 3588 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3589 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { if( pulTotalRunTime != 0 ) { @@ -12884,7 +12892,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", 3615, "( xIdleTaskHandle != 0 )") : (void)0); + (__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3616, "( xIdleTaskHandle != 0 )") : (void)0); return &( xIdleTaskHandle[ 0 ] ); } @@ -12895,7 +12903,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. */ -// # 3639 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3640 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp ) @@ -12904,7 +12912,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", 3647, "uxSchedulerSuspended == 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3648, "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(). */ @@ -12923,7 +12931,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", 3666, "pxTCB") : (void)0); + (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3667, "pxTCB") : (void)0); vTaskSuspendAll(); { @@ -13022,7 +13030,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 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3765, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); }; + { List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3766, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); }; } else { @@ -13205,13 +13213,13 @@ BaseType_t xTaskIncrementTick( void ) return xSwitchRequired; } /*-----------------------------------------------------------*/ -// # 3977 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 3978 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 4001 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4002 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 4026 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4027 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 4059 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4060 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ void vTaskSwitchContext( BaseType_t xCoreID ) @@ -13229,7 +13237,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", 4076, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0); + (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4077, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0); if( uxSchedulerSuspended != ( UBaseType_t ) ( ( char ) 0 ) ) { @@ -13241,7 +13249,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) { xYieldPendings[ xCoreID ] = ( ( char ) 0 ); ; -// # 4117 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4118 "/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 ); } }; @@ -13258,7 +13266,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) ; /* After the new task is switched in, update the global errno. */ -// # 4151 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4152 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } vPortRecursiveLock(0, spin_lock_instance(14), ( ( char ) 0 )); @@ -13269,7 +13277,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", 4161, "pxEventList") : (void)0); + (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4162, "pxEventList") : (void)0); /* THIS FUNCTION MUST BE CALLED WITH EITHER INTERRUPTS DISABLED OR THE * SCHEDULER SUSPENDED AND THE QUEUE BEING ACCESSED LOCKED. */ @@ -13288,11 +13296,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", 4180, "pxEventList") : (void)0); + (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4181, "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", 4184, "uxSchedulerSuspended != 0") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4185, "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 @@ -13316,7 +13324,7 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely ) { - (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4208, "pxEventList") : (void)0); + (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4209, "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 @@ -13364,14 +13372,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", 4256, "pxUnblockedTCB") : (void)0); + (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4257, "pxUnblockedTCB") : (void)0); ( void ) uxListRemove( &( pxUnblockedTCB->xEventListItem ) ); if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) ) { ( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) ); ; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ; -// # 4277 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4278 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } else { @@ -13401,7 +13409,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 != ( ( char ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4306, "uxSchedulerSuspended != ( ( char ) 0 )") : (void)0); + (__builtin_expect(!(uxSchedulerSuspended != ( ( char ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4307, "uxSchedulerSuspended != ( ( char ) 0 )") : (void)0); /* Store the new item value in the event list. */ ( ( pxEventListItem )->xItemValue = ( xItemValue | 0x80000000UL ) ); @@ -13409,9 +13417,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", 4314, "pxUnblockedTCB") : (void)0); + (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4315, "pxUnblockedTCB") : (void)0); ( void ) uxListRemove( pxEventListItem ); -// # 4331 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4332 "/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. */ @@ -13430,7 +13438,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem, void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut ) { - (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4349, "pxTimeOut") : (void)0); + (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4350, "pxTimeOut") : (void)0); vTaskEnterCritical(); { pxTimeOut->xOverflowCount = xNumOfOverflows; @@ -13453,8 +13461,8 @@ BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, { BaseType_t xReturn; - (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4372, "pxTimeOut") : (void)0); - (__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4373, "pxTicksToWait") : (void)0); + (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4373, "pxTimeOut") : (void)0); + (__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4374, "pxTicksToWait") : (void)0); vTaskEnterCritical(); { @@ -13576,7 +13584,7 @@ void vTaskMissedYield( void ) * * @todo additional conditional compiles to remove this function. */ -// # 4555 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4556 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /* * ----------------------------------------------------------- * The Idle task. @@ -13606,7 +13614,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(); -// # 4596 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4597 "/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 @@ -13627,16 +13635,16 @@ static void prvIdleTask( void * pvParameters ) ; } } -// # 4632 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4633 "/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. */ -// # 4697 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4698 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } } /*-----------------------------------------------------------*/ -// # 4747 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4748 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -13650,7 +13658,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", 4760, "pxTCB != 0") : (void)0); + (__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4761, "pxTCB != 0") : (void)0); pxTCB->pvThreadLocalStoragePointers[ xIndex ] = pvValue; } } @@ -13681,7 +13689,7 @@ static void prvIdleTask( void * pvParameters ) /*-----------------------------------------------------------*/ -// # 4807 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4808 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvInitialiseTaskLists( void ) @@ -13783,7 +13791,7 @@ static void prvCheckTasksWaitingTermination( void ) { pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority; } -// # 4919 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 4920 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { pxTaskStatus->ulRunTimeCounter = 0; } @@ -13914,7 +13922,7 @@ static void prvCheckTasksWaitingTermination( void ) /*-----------------------------------------------------------*/ -// # 5088 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5089 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ @@ -13971,7 +13979,7 @@ static void prvCheckTasksWaitingTermination( void ) free( (void*) pxTCB->pxStack); free( (void*) pxTCB); } -// # 5171 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5172 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" } @@ -14176,8 +14184,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", 5375, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0); - (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5376, "pxTCB->uxMutexesHeld") : (void)0); + (__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5376, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0); + (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5377, "pxTCB->uxMutexesHeld") : (void)0); ( pxTCB->uxMutexesHeld )--; /* Has the holder of the mutex inherited the priority of another @@ -14263,7 +14271,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", 5462, "pxTCB->uxMutexesHeld") : (void)0); + (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5463, "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 @@ -14290,7 +14298,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", 5489, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0); + (__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5490, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0); /* Disinherit the priority, remembering the previous * priority to facilitate determining the subject task's @@ -14421,7 +14429,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", 5620, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0); + (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5621, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0); if( xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U ) { @@ -14471,11 +14479,11 @@ void vTaskYieldWithinAPI( void ) /*-----------------------------------------------------------*/ -// # 5696 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5697 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ -// # 5802 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5803 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*----------------------------------------------------------*/ -// # 5929 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 5930 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ TickType_t uxTaskResetEventItemValue( void ) @@ -14517,7 +14525,7 @@ TickType_t uxTaskResetEventItemValue( void ) { uint32_t ulReturn; - (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5970, "uxIndexToWait < 1") : (void)0); + (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5971, "uxIndexToWait < 1") : (void)0); vTaskEnterCritical(); { @@ -14591,7 +14599,7 @@ TickType_t uxTaskResetEventItemValue( void ) { BaseType_t xReturn; - (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6044, "uxIndexToWait < 1") : (void)0); + (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6045, "uxIndexToWait < 1") : (void)0); vTaskEnterCritical(); { @@ -14679,8 +14687,8 @@ TickType_t uxTaskResetEventItemValue( void ) BaseType_t xReturn = ( ( ( char ) 1 ) ); uint8_t ucOriginalNotifyState; - (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6132, "uxIndexToNotify < 1") : (void)0); - (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6133, "xTaskToNotify") : (void)0); + (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6133, "uxIndexToNotify < 1") : (void)0); + (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6134, "xTaskToNotify") : (void)0); pxTCB = xTaskToNotify; vTaskEnterCritical(); @@ -14733,7 +14741,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", 6186, "xTickCount == ( TickType_t ) 0") : (void)0); + (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6187, "xTickCount == ( TickType_t ) 0") : (void)0); break; } @@ -14748,8 +14756,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", 6201, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); -// # 6220 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" + (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6202, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); +// # 6221 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" { prvYieldForTask( pxTCB, ( ( char ) 0 ) ); } @@ -14782,8 +14790,8 @@ TickType_t uxTaskResetEventItemValue( void ) BaseType_t xReturn = ( ( ( char ) 1 ) ); UBaseType_t uxSavedInterruptStatus; - (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6252, "xTaskToNotify") : (void)0); - (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6253, "uxIndexToNotify < 1") : (void)0); + (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6253, "xTaskToNotify") : (void)0); + (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6254, "uxIndexToNotify < 1") : (void)0); /* RTOS ports that support interrupt nesting have the concept of a * maximum system call (or maximum API call) interrupt priority. @@ -14854,7 +14862,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", 6324, "xTickCount == ( TickType_t ) 0") : (void)0); + (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6325, "xTickCount == ( TickType_t ) 0") : (void)0); break; } @@ -14865,7 +14873,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", 6335, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); + (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6336, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) ) { @@ -14910,8 +14918,8 @@ TickType_t uxTaskResetEventItemValue( void ) uint8_t ucOriginalNotifyState; UBaseType_t uxSavedInterruptStatus; - (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6380, "xTaskToNotify") : (void)0); - (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6381, "uxIndexToNotify < 1") : (void)0); + (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6381, "xTaskToNotify") : (void)0); + (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6382, "uxIndexToNotify < 1") : (void)0); /* RTOS ports that support interrupt nesting have the concept of a * maximum system call (or maximum API call) interrupt priority. @@ -14949,7 +14957,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", 6419, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); + (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6420, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0); if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) ) { @@ -14990,7 +14998,7 @@ TickType_t uxTaskResetEventItemValue( void ) TCB_t * pxTCB; BaseType_t xReturn; - (__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6460, "uxIndexToClear < 1") : (void)0); + (__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6461, "uxIndexToClear < 1") : (void)0); /* If null is passed in here then it is the calling task that is having * its notification state cleared. */ @@ -15043,7 +15051,7 @@ TickType_t uxTaskResetEventItemValue( void ) /*-----------------------------------------------------------*/ -// # 6529 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6530 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" /*-----------------------------------------------------------*/ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, @@ -15119,7 +15127,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, } } } -// # 6641 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" +// # 6642 "/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/snippets/rp2040_port_c_snippets.c b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c index 000c7b966..fad6c90bc 100644 --- a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c +++ b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c @@ -70,54 +70,7 @@ static void vPortStartFirstTask( void ) __attribute__( ( naked ) ); */ static void prvTaskExitError( void ); -/*@ -// Represents a stack that grows down. -predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) = - integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*& - ulStackDepth > 0 &*& - freeCells >= 0 &*& - pxTopOfStack == pxStack + freeCells -1 &*& - 0 <= freeCells &*& freeCells <= ulStackDepth; -// usedMem == pxStack - pxTopOfStack -// freeMem == ulStackDepth - usedMem - //freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*& -// usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack); -@*/ -/*/@ -lemma void split_stack(StackType_t * pxStack, int offset) -requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*& - offset * sizeof(StackType_t) < ulStackDepth; -ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*& - integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ; -{ - open stack_p(_, _, _, _); - integers__split(pxStack, offset * sizeof(StackType_t) ); -} -@*/ - -/*@ -lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack) -requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*& - freeCells > 0; -ensures // free cells minus top cell - integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _) &*& - // top stack cell - integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*& - // used stack cells - integers_(pxStack + freeCells, sizeof(StackType_t), false, - ulStackDepth - freeCells, _) &*& - // stack contraints necessary to close `stack_p` again - ulStackDepth > 0 &*& - freeCells >= 0 &*& - pxTopOfStack == pxStack + freeCells -1 &*& - 0 <= freeCells &*& freeCells <= ulStackDepth; -{ - open stack_p(_, _, _, _); - integers__split(pxStack, freeCells-1); - open integers_(pxStack + (freeCells-1), _, _, _, _); -} -@*/ // ------------------------------------------------- diff --git a/verification/verifast/proof/stack_predicates.h b/verification/verifast/proof/stack_predicates.h new file mode 100644 index 000000000..4375451ba --- /dev/null +++ b/verification/verifast/proof/stack_predicates.h @@ -0,0 +1,56 @@ +#ifndef STACK_PREDICATES +#define STACK_PREDICATES + + +/*@ +// Represents a stack that grows down (cf. RP2040 stack) +predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) = + integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*& + ulStackDepth > 0 &*& + freeCells >= 0 &*& + pxTopOfStack == pxStack + freeCells -1 &*& + 0 <= freeCells &*& freeCells <= ulStackDepth; +// usedMem == pxStack - pxTopOfStack +// freeMem == ulStackDepth - usedMem + //freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*& +// usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack); +@*/ + +/*/@ +lemma void split_stack(StackType_t * pxStack, int offset) +requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*& + offset * sizeof(StackType_t) < ulStackDepth; +ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*& + integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ; +{ + open stack_p(_, _, _, _); + integers__split(pxStack, offset * sizeof(StackType_t) ); +} +@*/ + +/*@ +// TODO: Do we need this lemma or is it usually cleaner to split stack manually? +lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack) +requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*& + freeCells > 0; +ensures // free cells minus top cell + integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _) &*& + // top stack cell + integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*& + // used stack cells + integers_(pxStack + freeCells, sizeof(StackType_t), false, + ulStackDepth - freeCells, _) &*& + // stack contraints necessary to close `stack_p` again + ulStackDepth > 0 &*& + freeCells >= 0 &*& + pxTopOfStack == pxStack + freeCells -1 &*& + 0 <= freeCells &*& freeCells <= ulStackDepth; +{ + open stack_p(_, _, _, _); + integers__split(pxStack, freeCells-1); + open integers_(pxStack + (freeCells-1), _, _, _, _); +} +@*/ + + +#endif /* STACK_PREDICATES */ \ No newline at end of file