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

Resolved VF parse error: VF does not support const pointers.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-22 13:00:58 -04:00
parent eeae596776
commit 342ab6463c
2 changed files with 281 additions and 214 deletions
Download patch file Download diff file Expand all files Collapse all files

42
tasks.c
View file

@ -869,7 +869,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE ) if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
{ {
List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] ); #ifdef VERIFAST
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
List_t * pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] );
#else
List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] );
#endif /* VERIFAST */
ListItem_t * pxLastTaskItem = pxReadyList->pxIndex->pxPrevious; ListItem_t * pxLastTaskItem = pxReadyList->pxIndex->pxPrevious;
ListItem_t * pxTaskItem = pxLastTaskItem; ListItem_t * pxTaskItem = pxLastTaskItem;
@ -1996,7 +2004,19 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
eTaskState eTaskGetState( TaskHandle_t xTask ) eTaskState eTaskGetState( TaskHandle_t xTask )
{ {
eTaskState eReturn; eTaskState eReturn;
List_t const * pxStateList, * pxDelayedList, * pxOverflowedDelayedList; #ifdef VERIFAST
/* Reason for rewrite:
* VeriFast does not support the following:
* - const pointers
* - multiple pointer declarations to user-defined types in single
* statement (i.e., `A p1, p2;` is ok, `A *p1, *p2;` fails)
*/
List_t * pxStateList;
List_t * pxDelayedList;
List_t * pxOverflowedDelayedList;
#else
List_t * pxStateList, * pxDelayedList, * pxOverflowedDelayedList;
#endif /* VERIFAST */
const TCB_t * const pxTCB = xTask; const TCB_t * const pxTCB = xTask;
configASSERT( pxTCB ); configASSERT( pxTCB );
@ -2092,7 +2112,14 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
UBaseType_t uxTaskPriorityGet( const TaskHandle_t xTask ) UBaseType_t uxTaskPriorityGet( const TaskHandle_t xTask )
{ {
TCB_t const * pxTCB; #ifdef VERIFAST
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
TCB_t * pxTCB;
#else
TCB_t const * pxTCB;
#endif /* VERIFAST */
UBaseType_t uxReturn; UBaseType_t uxReturn;
taskENTER_CRITICAL(); taskENTER_CRITICAL();
@ -2114,7 +2141,14 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
UBaseType_t uxTaskPriorityGetFromISR( const TaskHandle_t xTask ) UBaseType_t uxTaskPriorityGetFromISR( const TaskHandle_t xTask )
{ {
TCB_t const * pxTCB; #ifdef VERIFAST
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
TCB_t * pxTCB;
#else
TCB_t const * pxTCB;
#endif /* VERIFAST */
UBaseType_t uxReturn, uxSavedInterruptState; UBaseType_t uxReturn, uxSavedInterruptState;
/* RTOS ports that support interrupt nesting have the concept of a /* RTOS ports that support interrupt nesting have the concept of a

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

File diff suppressed because it is too large Load diff