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

Paused partial proof for xTaskCreate.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-07 14:40:08 -05:00
parent c4f5c09a81
commit 9fa8c76447
1 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
tasks.c
View file

@ -1431,6 +1431,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
}
#endif
/* TODO: Continue proof
* For now we stop verification here and concentrate on new
* verification target.
*/
//@ assume(false);
prvAddNewTaskToReadyList( pxNewTCB );
xReturn = pdPASS;
}
@ -1876,10 +1882,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
/*-----------------------------------------------------------*/
static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
/*@ requires interruptState_p(?coreID, _) &*&
/*//@ requires interruptState_p(?coreID, _) &*&
unprotectedGlobalVars();
@*/
/*@ ensures true;
/*//@ ensures true;
@*/
{
/* Ensure interrupts don't access the task lists while the lists are being
@ -5284,8 +5290,8 @@ static void prvResetNextTaskUnblockTime( void )
#if ( ( INCLUDE_xTaskGetCurrentTaskHandle == 1 ) || ( configUSE_MUTEXES == 1 ) )
TaskHandle_t xTaskGetCurrentTaskHandle( void )
//@ requires interruptState_p(?coreID, ?irpState);
//@ ensures interruptState_p(coreID, irpState) &*& false;
///@ requires interruptState_p(?coreID, ?irpState);
///@ ensures interruptState_p(coreID, irpState) &*& false;
{
TaskHandle_t xReturn;
uint32_t ulState;
@ -5662,8 +5668,8 @@ void vTaskYieldWithinAPI( void )
#if ( portCRITICAL_NESTING_IN_TCB == 1 )
void vTaskEnterCritical( void )
//@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars();
//@ ensures false;
///@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars();
///@ ensures false;
{
portDISABLE_INTERRUPTS();
//@ open unprotectedGlobalVars();