len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 22:25:14 -05:00
Code Issues Projects Releases Packages Wiki Activity

Added snippet from RP2040 port.c to verification code base to allow verification of contract from portable.h

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-26 10:08:29 -04:00
parent 8bb4f13ae5
commit b5f0b2f74d
7 changed files with 268 additions and 126 deletions
Download patch file Download diff file Expand all files Collapse all files

2
include/portable.h
View file

@ -128,6 +128,8 @@
StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
TaskFunction_t pxCode,
void * pvParameters ) PRIVILEGED_FUNCTION;
//@ requires true;
//@ ensures true;
#endif
#endif /* if ( portUSING_MPU_WRAPPERS == 1 ) */

2
portable/ThirdParty/GCC/RP2040/port.c vendored
View file

@ -170,6 +170,8 @@ static uint8_t ucPrimaryCoreNum = INVALID_PRIMARY_CORE_NUM;
StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
TaskFunction_t pxCode,
void * pvParameters )
//@ requires true;
//@ ensures true;
{
/* Simulate the stack frame as it would be created by a context switch
* interrupt. */

2
tasks.c
View file

@ -51,6 +51,8 @@
#include "verifast_RP2040_axioms.h"
#include "verifast_prelude_extended.h"
#include "verifast_asm.h"
#include "snippets/rp2040_port_c_snippets.c"
#endif
/* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified

1
verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh
View file

@ -49,6 +49,7 @@ clang -E -C -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS
-I"$PROOF_FILES_DIR" \
-I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/OnEitherCore" \
-I"$REPO_BASE_DIR/portable/ThirdParty/GCC/RP2040/include" \
-I"$REPO_BASE_DIR/portable/ThirdParty/GCC/RP2040" \
-I"$REPO_BASE_DIR/include" \
-I"$PICO_SDK_DIR/src/common/pico_base/include" \
-I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/build/generated/pico_base" \

314
verification/verifast/preprocessed_files/tasks--pp.c
View file

@ -4449,6 +4449,8 @@ bool spin_lock_is_claimed(uint lock_num);
StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
TaskFunction_t pxCode,
void * pvParameters ) ;
//@ requires true;
//@ ensures true;
@ -4504,11 +4506,11 @@ void vPortGetHeapStats( HeapStats_t * pxHeapStats );
* Reversely, calling `free` cleans up all the predicates instantiated
* by `malloc`.
*/
// # 197 "/Users/reitobia/repos2/FreeRTOS-Kernel/include/portable.h"
// # 199 "/Users/reitobia/repos2/FreeRTOS-Kernel/include/portable.h"
void vPortInitialiseBlocks( void ) ;
size_t xPortGetFreeHeapSize( void ) ;
size_t xPortGetMinimumEverFreeHeapSize( void ) ;
// # 209 "/Users/reitobia/repos2/FreeRTOS-Kernel/include/portable.h"
// # 211 "/Users/reitobia/repos2/FreeRTOS-Kernel/include/portable.h"
/*
* Setup the hardware ready for the scheduler to take control. This generally
* sets up a tick interrupt and sets timers for the correct tick frequency.
@ -4529,7 +4531,7 @@ void vPortEndScheduler( void ) ;
* Fills the xMPUSettings structure with the memory region information
* contained in xRegions.
*/
// # 237 "/Users/reitobia/repos2/FreeRTOS-Kernel/include/portable.h"
// # 239 "/Users/reitobia/repos2/FreeRTOS-Kernel/include/portable.h"
/* *INDENT-OFF* */
@ -10115,6 +10117,68 @@ bool assert_fct(bool b)
*/
// # 54 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2
// # 1 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/snippets/rp2040_port_c_snippets.c" 1
/*
* This file contains code snippets from:
* portable/ThirdParty/GCC/RP2040/port.c
*/
// Note currently we support configNUM_CORES == 1 with SMP, thought it isn't 100% clear why you wouldn't
// just use the non SMP version; keeping around for now in case the code bases are merged.
/* Constants required to manipulate the NVIC. */
// # 27 "/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof/snippets/rp2040_port_c_snippets.c"
/* Constants required to set up the initial stack. */
/* The systick is a 24-bit counter. */
/* A fiddle factor to estimate the number of SysTick counts that would have
* occurred while the SysTick counter is stopped during tickless idle
* calculations. */
/* Let the user override the pre-loading of the initial LR with the address of
* prvTaskExitError() in case it messes up unwinding of the stack in the
* debugger. */
/*
* See header file for description.
*/
StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
TaskFunction_t pxCode,
void * pvParameters )
//@ requires true;
//@ ensures true;
{
/* Simulate the stack frame as it would be created by a context switch
* interrupt. */
pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
*pxTopOfStack = ( 0x01000000 ); /* xPSR */
pxTopOfStack--;
*pxTopOfStack = ( StackType_t ) pxCode; /* PC */
pxTopOfStack--;
*pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */
pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
*pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
pxTopOfStack -= 8; /* R11..R4. */
return pxTopOfStack;
}
// # 56 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2
/* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified
* because the MPU ports require MPU_WRAPPERS_INCLUDED_FROM_API_FILE to be defined
@ -10124,7 +10188,7 @@ bool assert_fct(bool b)
/* Set configUSE_STATS_FORMATTING_FUNCTIONS to 2 to include the stats formatting
* functions but without including stdio.h here. */
// # 82 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 84 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/* Values that can be assigned to the ucNotifyState member of the TCB. */
@ -10181,18 +10245,18 @@ bool assert_fct(bool b)
/* uxTopReadyPriority holds the priority of the highest priority ready
* state task. */
// # 146 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 148 "/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. */
// # 180 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 182 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
/* pxDelayedTaskList and pxOverflowDelayedTaskList are switched when the tick
* count overflows. */
// # 198 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 200 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
/*
@ -10247,7 +10311,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. */
// # 261 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 263 "/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. */
@ -10255,7 +10319,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. */
// # 278 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 280 "/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. */
@ -10275,7 +10339,7 @@ typedef struct tskTaskControlBlock /* The old naming convention is used to preve
void * pvThreadLocalStoragePointers[ 5 ];
// # 318 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 320 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
volatile uint32_t ulNotifiedValue[ 1 ];
volatile uint8_t ucNotifyState[ 1 ];
@ -10366,7 +10430,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 );
// # 418 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 420 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*lint -restore */
/*-----------------------------------------------------------*/
@ -10519,7 +10583,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
* will exit the Blocked state.
*/
static void prvResetNextTaskUnblockTime( void ) ;
// # 582 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 584 "/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.
@ -10551,9 +10615,9 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) ;
/*-----------------------------------------------------------*/
// # 632 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 634 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 715 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 717 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
static void prvYieldCore( BaseType_t xCoreID )
@ -10595,8 +10659,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", 756, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
// # 769 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
(__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"
xLowestPriority = ( BaseType_t ) pxTCB->uxPriority;
if( xPreemptEqualPriority == ( ( char ) 0 ) )
@ -10635,7 +10699,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
{
;
}
// # 823 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 825 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
else
{
@ -10648,7 +10712,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
prvYieldCore( xLowestPriorityCore );
xYieldCount++;
}
// # 843 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 845 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
/*-----------------------------------------------------------*/
@ -10659,10 +10723,10 @@ static void prvYieldForTask( TCB_t * pxTCB,
UBaseType_t uxCurrentPriority = uxTopReadyPriority;
BaseType_t xTaskScheduled = ( ( char ) 0 );
BaseType_t xDecrementTopPriority = ( ( char ) 1 );
// # 861 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 863 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
while( xTaskScheduled == ( ( char ) 0 ) )
{
// # 875 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 877 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
if( ( ( ( &( pxReadyTasksLists[ uxCurrentPriority ] ) )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) == ( ( char ) 0 ) )
{
@ -10700,7 +10764,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() ); */
// # 928 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 930 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
if( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -1 ) )
{
@ -10721,7 +10785,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", 948, "( 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", 950, "( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == ( TaskRunning_t ) ( -2 ) )") : (void)0);
@ -10765,21 +10829,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", 992, "( 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", 994, "( 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", 996, "( ( 0 <= pxCurrentTCBs[ xCoreID ]->xTaskRunState ) && ( pxCurrentTCBs[ xCoreID ]->xTaskRunState < 1 ) )") : (void)0);
// # 1072 "/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", 998, "( ( 0 <= pxCurrentTCBs[ xCoreID ]->xTaskRunState ) && ( pxCurrentTCBs[ xCoreID ]->xTaskRunState < 1 ) )") : (void)0);
// # 1074 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
return ( ( char ) 1 );
}
// # 1088 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1090 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 1166 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1168 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 1229 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1231 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 1295 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1297 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -10796,7 +10860,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
chars(pcName, 16, _);
@*/
//@ ensures true;
// # 1324 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1326 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
TCB_t * pxNewTCB;
BaseType_t xReturn;
@ -10804,7 +10868,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. */
// # 1354 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1356 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
StackType_t * pxStack;
@ -10840,9 +10904,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
if( pxNewTCB != 0 )
{
// # 1397 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1399 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
prvInitialiseNewTask( pxTaskCode, pcName, ( uint32_t ) usStackDepth, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0 );
// # 1406 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1408 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
prvAddNewTaskToReadyList( pxNewTCB );
xReturn = ( ( ( char ) 1 ) );
}
@ -10880,7 +10944,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
{
StackType_t * pxTopOfStack;
UBaseType_t x;
// # 1460 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1462 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
//@ open TCB_p(_,_);
/* Avoid dependency on memset() if it is not required. */
@ -10927,9 +10991,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. */
// # 1520 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1522 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
// # 1534 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1536 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
//@ close TCB_p(pxNewTCB, stackSize);
/* Store the task name in the TCB. */
@ -11019,7 +11083,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
{
pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U;
}
// # 1642 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1644 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
/* Avoid compiler warning about unreferenced parameter. */
( void ) xRegions;
@ -11046,7 +11110,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
//@ uchars__to_chars_(pxNewTCB->ucNotifyState);
memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) );
}
// # 1680 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1682 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
/* Reason for rewrite: Assignment not type safe. */
@ -11055,17 +11119,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
}
// # 1703 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1705 "/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. */
// # 1731 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1733 "/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. */
// # 1748 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 1750 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters );
}
@ -11276,7 +11340,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
if( xTaskRunningOnCore == xCoreID )
{
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1958, "uxSchedulerSuspended == 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1960, "uxSchedulerSuspended == 0") : (void)0);
vTaskYieldWithinAPI();
}
else
@ -11299,12 +11363,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", 1981, "pxPreviousWakeTime") : (void)0);
(__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1982, "( xTimeIncrement > 0U )") : (void)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);
vTaskSuspendAll();
{
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1986, "uxSchedulerSuspended == 1") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1988, "uxSchedulerSuspended == 1") : (void)0);
/* Minor optimisation. The tick count cannot change in this
* block. */
@ -11390,7 +11454,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
{
vTaskSuspendAll();
{
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2072, "uxSchedulerSuspended == 1") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2074, "uxSchedulerSuspended == 1") : (void)0);
;
/* A task that is removed from the event list while the
@ -11444,7 +11508,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
const TCB_t * const pxTCB = xTask;
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2126, "pxTCB") : (void)0);
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2128, "pxTCB") : (void)0);
vTaskEnterCritical();
{
@ -11620,7 +11684,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", 2302, "( uxNewPriority < 32 )") : (void)0);
(__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2304, "( uxNewPriority < 32 )") : (void)0);
/* Ensure the new priority is valid. */
if( uxNewPriority >= ( UBaseType_t ) 32 )
@ -11774,13 +11838,13 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
/*-----------------------------------------------------------*/
// # 2490 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2492 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 2513 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2515 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 2531 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2533 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 2559 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2561 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -11857,7 +11921,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", 2635, "uxSchedulerSuspended == 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2637, "uxSchedulerSuspended == 0") : (void)0);
vTaskYieldWithinAPI();
}
else
@ -11871,7 +11935,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
{
vTaskExitCritical();
(__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2649, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0);
(__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2651, "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
@ -11918,7 +11982,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", 2696, "xTask") : (void)0);
(__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2698, "xTask") : (void)0);
/* Is the task being resumed actually in the suspended list? */
if( ( ( ( &( pxTCB->xStateListItem ) )->pxContainer == ( &xSuspendedTaskList ) ) ? ( ( ( char ) 1 ) ) : ( ( ( char ) 0 ) ) ) != ( ( char ) 0 ) )
@ -11967,7 +12031,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", 2745, "xTaskToResume") : (void)0);
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2747, "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
@ -12026,7 +12090,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
UBaseType_t uxSavedInterruptStatus;
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2804, "xTaskToResume") : (void)0);
(__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2806, "xTaskToResume") : (void)0);
/* RTOS ports that support interrupt nesting have the concept of a
* maximum system call (or maximum API call) interrupt priority.
@ -12147,7 +12211,7 @@ static BaseType_t prvCreateIdleTasks( void )
{
;
}
// # 2972 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2974 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
if( xCoreID == 0 )
{
@ -12159,7 +12223,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. */
}
// # 2995 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 2997 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
}
@ -12196,7 +12260,7 @@ void vTaskStartScheduler( void )
* so interrupts will automatically get re-enabled when the first task
* starts to run. */
assert_fct(false);
// # 3045 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3047 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL;
xSchedulerRunning = ( ( char ) 1 );
xTickCount = ( TickType_t ) 0;
@ -12228,7 +12292,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", 3076, "xReturn != ( -1 )") : (void)0);
(__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3078, "xReturn != ( -1 )") : (void)0);
}
/* Prevent compiler warnings if INCLUDE_xTaskGetIdleTaskHandle is set to 0,
@ -12293,7 +12357,7 @@ void vTaskSuspendAll( void )
}
}
/*----------------------------------------------------------*/
// # 3203 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3205 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/
BaseType_t xTaskResumeAll( void )
@ -12316,7 +12380,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", 3225, "uxSchedulerSuspended") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3227, "uxSchedulerSuspended") : (void)0);
--uxSchedulerSuspended;
vPortRecursiveLock(1, spin_lock_instance(15), ( ( char ) 0 ));
@ -12474,7 +12538,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", 3383, "pxTCB") : (void)0);
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3385, "pxTCB") : (void)0);
return &( pxTCB->pcTaskName[ 0 ] );
}
/*-----------------------------------------------------------*/
@ -12567,7 +12631,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", 3476, "strlen( pcNameToQuery ) < 16") : (void)0);
(__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3478, "strlen( pcNameToQuery ) < 16") : (void)0);
vTaskSuspendAll();
{
@ -12663,7 +12727,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
* each task in the Suspended state. */
uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended );
}
// # 3586 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3588 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
if( pulTotalRunTime != 0 )
{
@ -12691,7 +12755,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", 3613, "( xIdleTaskHandle != 0 )") : (void)0);
(__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3615, "( xIdleTaskHandle != 0 )") : (void)0);
return &( xIdleTaskHandle[ 0 ] );
}
@ -12702,7 +12766,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. */
// # 3637 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3639 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/
BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
@ -12711,7 +12775,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", 3645, "uxSchedulerSuspended == 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3647, "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(). */
@ -12730,7 +12794,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", 3664, "pxTCB") : (void)0);
(__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3666, "pxTCB") : (void)0);
vTaskSuspendAll();
{
@ -12829,7 +12893,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", 3763, "( ( ( ( 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", 3765, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); };
}
else
{
@ -13012,13 +13076,13 @@ BaseType_t xTaskIncrementTick( void )
return xSwitchRequired;
}
/*-----------------------------------------------------------*/
// # 3975 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 3977 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 3999 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4001 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 4024 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4026 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 4057 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4059 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
void vTaskSwitchContext( BaseType_t xCoreID )
@ -13036,7 +13100,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", 4074, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0);
(__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4076, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0);
if( uxSchedulerSuspended != ( UBaseType_t ) ( ( char ) 0 ) )
{
@ -13048,7 +13112,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
{
xYieldPendings[ xCoreID ] = ( ( char ) 0 );
;
// # 4115 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4117 "/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 ); } };
@ -13065,7 +13129,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
;
/* After the new task is switched in, update the global errno. */
// # 4149 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4151 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
}
vPortRecursiveLock(0, spin_lock_instance(14), ( ( char ) 0 ));
@ -13076,7 +13140,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", 4159, "pxEventList") : (void)0);
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4161, "pxEventList") : (void)0);
/* THIS FUNCTION MUST BE CALLED WITH EITHER INTERRUPTS DISABLED OR THE
* SCHEDULER SUSPENDED AND THE QUEUE BEING ACCESSED LOCKED. */
@ -13095,11 +13159,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", 4178, "pxEventList") : (void)0);
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4180, "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", 4182, "uxSchedulerSuspended != 0") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4184, "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
@ -13123,7 +13187,7 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList,
TickType_t xTicksToWait,
const BaseType_t xWaitIndefinitely )
{
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4206, "pxEventList") : (void)0);
(__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4208, "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
@ -13171,14 +13235,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", 4254, "pxUnblockedTCB") : (void)0);
(__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4256, "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 ) ); ;
// # 4275 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4277 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
else
{
@ -13208,7 +13272,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", 4304, "uxSchedulerSuspended != ( ( char ) 0 )") : (void)0);
(__builtin_expect(!(uxSchedulerSuspended != ( ( char ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4306, "uxSchedulerSuspended != ( ( char ) 0 )") : (void)0);
/* Store the new item value in the event list. */
( ( pxEventListItem )->xItemValue = ( xItemValue | 0x80000000UL ) );
@ -13216,9 +13280,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", 4312, "pxUnblockedTCB") : (void)0);
(__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4314, "pxUnblockedTCB") : (void)0);
( void ) uxListRemove( pxEventListItem );
// # 4329 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4331 "/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. */
@ -13237,7 +13301,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut )
{
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4347, "pxTimeOut") : (void)0);
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4349, "pxTimeOut") : (void)0);
vTaskEnterCritical();
{
pxTimeOut->xOverflowCount = xNumOfOverflows;
@ -13260,8 +13324,8 @@ BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
{
BaseType_t xReturn;
(__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4370, "pxTimeOut") : (void)0);
(__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4371, "pxTicksToWait") : (void)0);
(__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);
vTaskEnterCritical();
{
@ -13383,7 +13447,7 @@ void vTaskMissedYield( void )
*
* @todo additional conditional compiles to remove this function.
*/
// # 4553 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4555 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*
* -----------------------------------------------------------
* The Idle task.
@ -13413,7 +13477,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();
// # 4594 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4596 "/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
@ -13434,16 +13498,16 @@ static void prvIdleTask( void * pvParameters )
;
}
}
// # 4630 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4632 "/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. */
// # 4695 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4697 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
}
/*-----------------------------------------------------------*/
// # 4745 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4747 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -13457,7 +13521,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", 4758, "pxTCB != 0") : (void)0);
(__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4760, "pxTCB != 0") : (void)0);
pxTCB->pvThreadLocalStoragePointers[ xIndex ] = pvValue;
}
}
@ -13488,7 +13552,7 @@ static void prvIdleTask( void * pvParameters )
/*-----------------------------------------------------------*/
// # 4805 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4807 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
static void prvInitialiseTaskLists( void )
@ -13590,7 +13654,7 @@ static void prvCheckTasksWaitingTermination( void )
{
pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority;
}
// # 4917 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 4919 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
{
pxTaskStatus->ulRunTimeCounter = 0;
}
@ -13721,7 +13785,7 @@ static void prvCheckTasksWaitingTermination( void )
/*-----------------------------------------------------------*/
// # 5086 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5088 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
@ -13778,7 +13842,7 @@ static void prvCheckTasksWaitingTermination( void )
free( (void*) pxTCB->pxStack);
free( (void*) pxTCB);
}
// # 5169 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5171 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
@ -13983,8 +14047,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", 5373, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0);
(__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5374, "pxTCB->uxMutexesHeld") : (void)0);
(__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);
( pxTCB->uxMutexesHeld )--;
/* Has the holder of the mutex inherited the priority of another
@ -14070,7 +14134,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", 5460, "pxTCB->uxMutexesHeld") : (void)0);
(__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5462, "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
@ -14097,7 +14161,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", 5487, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0);
(__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5489, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0);
/* Disinherit the priority, remembering the previous
* priority to facilitate determining the subject task's
@ -14228,7 +14292,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", 5618, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
(__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5620, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
if( xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U )
{
@ -14278,11 +14342,11 @@ void vTaskYieldWithinAPI( void )
/*-----------------------------------------------------------*/
// # 5694 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5696 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
// # 5800 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5802 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*----------------------------------------------------------*/
// # 5927 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 5929 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
TickType_t uxTaskResetEventItemValue( void )
@ -14324,7 +14388,7 @@ TickType_t uxTaskResetEventItemValue( void )
{
uint32_t ulReturn;
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5968, "uxIndexToWait < 1") : (void)0);
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5970, "uxIndexToWait < 1") : (void)0);
vTaskEnterCritical();
{
@ -14398,7 +14462,7 @@ TickType_t uxTaskResetEventItemValue( void )
{
BaseType_t xReturn;
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6042, "uxIndexToWait < 1") : (void)0);
(__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6044, "uxIndexToWait < 1") : (void)0);
vTaskEnterCritical();
{
@ -14486,8 +14550,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", 6130, "uxIndexToNotify < 1") : (void)0);
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6131, "xTaskToNotify") : (void)0);
(__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);
pxTCB = xTaskToNotify;
vTaskEnterCritical();
@ -14540,7 +14604,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", 6184, "xTickCount == ( TickType_t ) 0") : (void)0);
(__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6186, "xTickCount == ( TickType_t ) 0") : (void)0);
break;
}
@ -14555,8 +14619,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", 6199, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
// # 6218 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
(__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"
{
prvYieldForTask( pxTCB, ( ( char ) 0 ) );
}
@ -14589,8 +14653,8 @@ TickType_t uxTaskResetEventItemValue( void )
BaseType_t xReturn = ( ( ( char ) 1 ) );
UBaseType_t uxSavedInterruptStatus;
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6250, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6251, "uxIndexToNotify < 1") : (void)0);
(__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);
/* RTOS ports that support interrupt nesting have the concept of a
* maximum system call (or maximum API call) interrupt priority.
@ -14661,7 +14725,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", 6322, "xTickCount == ( TickType_t ) 0") : (void)0);
(__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6324, "xTickCount == ( TickType_t ) 0") : (void)0);
break;
}
@ -14672,7 +14736,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", 6333, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6335, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) )
{
@ -14717,8 +14781,8 @@ TickType_t uxTaskResetEventItemValue( void )
uint8_t ucOriginalNotifyState;
UBaseType_t uxSavedInterruptStatus;
(__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6378, "xTaskToNotify") : (void)0);
(__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6379, "uxIndexToNotify < 1") : (void)0);
(__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);
/* RTOS ports that support interrupt nesting have the concept of a
* maximum system call (or maximum API call) interrupt priority.
@ -14756,7 +14820,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", 6417, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
(__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6419, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) )
{
@ -14797,7 +14861,7 @@ TickType_t uxTaskResetEventItemValue( void )
TCB_t * pxTCB;
BaseType_t xReturn;
(__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6458, "uxIndexToClear < 1") : (void)0);
(__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6460, "uxIndexToClear < 1") : (void)0);
/* If null is passed in here then it is the calling task that is having
* its notification state cleared. */
@ -14850,7 +14914,7 @@ TickType_t uxTaskResetEventItemValue( void )
/*-----------------------------------------------------------*/
// # 6527 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 6529 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
/*-----------------------------------------------------------*/
static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
@ -14926,7 +14990,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
}
}
}
// # 6639 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
// # 6641 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
}
/* Code below here allows additional code to be inserted into this source file,

72
verification/verifast/proof/snippets/rp2040_port_c_snippets.c Normal file
View file

@ -0,0 +1,72 @@
/*
* This file contains code snippets from:
* portable/ThirdParty/GCC/RP2040/port.c
*/
// Note currently we support configNUM_CORES == 1 with SMP, thought it isn't 100% clear why you wouldn't
// just use the non SMP version; keeping around for now in case the code bases are merged.
#define portRUNNING_ON_BOTH_CORES (configNUM_CORES == portMAX_CORE_COUNT)
/* Constants required to manipulate the NVIC. */
#define portNVIC_SYSTICK_CTRL_REG ( *( ( volatile uint32_t * ) 0xe000e010 ) )
#define portNVIC_SYSTICK_LOAD_REG ( *( ( volatile uint32_t * ) 0xe000e014 ) )
#define portNVIC_SYSTICK_CURRENT_VALUE_REG ( *( ( volatile uint32_t * ) 0xe000e018 ) )
#define portNVIC_INT_CTRL_REG ( *( ( volatile uint32_t * ) 0xe000ed04 ) )
#define portNVIC_SHPR3_REG ( *( ( volatile uint32_t * ) 0xe000ed20 ) )
#define portNVIC_SYSTICK_CLK_BIT ( 1UL << 2UL )
#define portNVIC_SYSTICK_INT_BIT ( 1UL << 1UL )
#define portNVIC_SYSTICK_ENABLE_BIT ( 1UL << 0UL )
#define portNVIC_SYSTICK_COUNT_FLAG_BIT ( 1UL << 16UL )
#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL )
#define portMIN_INTERRUPT_PRIORITY ( 255UL )
#define portNVIC_PENDSV_PRI ( portMIN_INTERRUPT_PRIORITY << 16UL )
#define portNVIC_SYSTICK_PRI ( portMIN_INTERRUPT_PRIORITY << 24UL )
/* Constants required to set up the initial stack. */
#define portINITIAL_XPSR ( 0x01000000 )
/* The systick is a 24-bit counter. */
#define portMAX_24_BIT_NUMBER ( 0xffffffUL )
/* A fiddle factor to estimate the number of SysTick counts that would have
* occurred while the SysTick counter is stopped during tickless idle
* calculations. */
#ifndef portMISSED_COUNTS_FACTOR
#define portMISSED_COUNTS_FACTOR ( 45UL )
#endif
/* Let the user override the pre-loading of the initial LR with the address of
* prvTaskExitError() in case it messes up unwinding of the stack in the
* debugger. */
#ifdef configTASK_RETURN_ADDRESS
#define portTASK_RETURN_ADDRESS configTASK_RETURN_ADDRESS
#else
#define portTASK_RETURN_ADDRESS prvTaskExitError
#endif
/*
* See header file for description.
*/
StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
TaskFunction_t pxCode,
void * pvParameters )
//@ requires true;
//@ ensures true;
{
/* Simulate the stack frame as it would be created by a context switch
* interrupt. */
pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
*pxTopOfStack = portINITIAL_XPSR; /* xPSR */
pxTopOfStack--;
*pxTopOfStack = ( StackType_t ) pxCode; /* PC */
pxTopOfStack--;
*pxTopOfStack = ( StackType_t ) portTASK_RETURN_ADDRESS; /* LR */
pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
*pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
pxTopOfStack -= 8; /* R11..R4. */
return pxTopOfStack;
}

1
verification/verifast/proof/task_predicates.h
View file

@ -41,7 +41,6 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
// We assume that the macro `configTASK_NOTIFICATION_ARRAY_ENTRIES`
// evaluates to 1.
integers__(tcb->ulNotifiedValue, 4, false, 1, _) &*&
uchars_(tcb->ucNotifyState, 1, _) &*&
tcb->ucDelayAborted |-> _;