Reverted manual VF rewrites concerning const pointers. Respective rewrites are applied during preprocessing.

This commit is contained in:
Tobias Reinhard 2022-11-11 15:44:23 -05:00
parent 0a31349be3
commit 7c9711cb88
2 changed files with 24 additions and 90 deletions

View file

@ -301,36 +301,18 @@ typedef struct xLIST
* \page listGET_OWNER_OF_NEXT_ENTRY listGET_OWNER_OF_NEXT_ENTRY * \page listGET_OWNER_OF_NEXT_ENTRY listGET_OWNER_OF_NEXT_ENTRY
* \ingroup LinkedList * \ingroup LinkedList
*/ */
#ifdef VERIFAST #define listGET_OWNER_OF_NEXT_ENTRY( pxTCB, pxList ) \
/* Reason for rewrite: { \
* VeriFast does not support const pointers. List_t * const pxConstList = ( pxList ); \
*/ /* Increment the index to the next item and return the item, ensuring */ \
#define listGET_OWNER_OF_NEXT_ENTRY( pxTCB, pxList ) \ /* we don't return the marker used at the end of the list. */ \
{ \ ( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext; \
List_t * pxConstList = ( pxList ); \ if( ( void * ) ( pxConstList )->pxIndex == ( void * ) &( ( pxConstList )->xListEnd ) ) \
/* Increment the index to the next item and return the item, ensuring */ \ { \
/* we don't return the marker used at the end of the list. */ \ ( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext; \
( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext; \ } \
if( ( void * ) ( pxConstList )->pxIndex == ( void * ) &( ( pxConstList )->xListEnd ) ) \ ( pxTCB ) = ( pxConstList )->pxIndex->pvOwner; \
{ \ }
( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext; \
} \
( pxTCB ) = ( pxConstList )->pxIndex->pvOwner; \
}
#else
#define listGET_OWNER_OF_NEXT_ENTRY( pxTCB, pxList ) \
{ \
List_t * const pxConstList = ( pxList ); \
/* Increment the index to the next item and return the item, ensuring */ \
/* we don't return the marker used at the end of the list. */ \
( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext; \
if( ( void * ) ( pxConstList )->pxIndex == ( void * ) &( ( pxConstList )->xListEnd ) ) \
{ \
( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext; \
} \
( pxTCB ) = ( pxConstList )->pxIndex->pvOwner; \
}
#endif /* VERIFAST */

72
tasks.c
View file

@ -897,14 +897,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE ) if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
{ {
#ifdef VERIFAST
/* Reason for rewrite: List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] );
* 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;
@ -2210,11 +2204,11 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
* - multiple pointer declarations to user-defined types in single * - multiple pointer declarations to user-defined types in single
* statement (i.e., `A p1, p2;` is ok, `A *p1, *p2;` fails) * statement (i.e., `A p1, p2;` is ok, `A *p1, *p2;` fails)
*/ */
List_t * pxStateList; List_t const * pxStateList;
List_t * pxDelayedList; List_t const * pxDelayedList;
List_t * pxOverflowedDelayedList; List_t const * pxOverflowedDelayedList;
#else #else
List_t * pxStateList, * pxDelayedList, * pxOverflowedDelayedList; List_t const * pxStateList, * pxDelayedList, * pxOverflowedDelayedList;
#endif /* VERIFAST */ #endif /* VERIFAST */
const TCB_t * const pxTCB = xTask; const TCB_t * const pxTCB = xTask;
@ -2311,14 +2305,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
UBaseType_t uxTaskPriorityGet( const TaskHandle_t xTask ) UBaseType_t uxTaskPriorityGet( const TaskHandle_t xTask )
{ {
#ifdef VERIFAST TCB_t const * pxTCB;
/* 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();
@ -2340,14 +2327,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
UBaseType_t uxTaskPriorityGetFromISR( const TaskHandle_t xTask ) UBaseType_t uxTaskPriorityGetFromISR( const TaskHandle_t xTask )
{ {
#ifdef VERIFAST TCB_t const * pxTCB;
/* 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
@ -2886,14 +2866,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
BaseType_t xTaskResumeFromISR( TaskHandle_t xTaskToResume ) BaseType_t xTaskResumeFromISR( TaskHandle_t xTaskToResume )
{ {
BaseType_t xYieldRequired = pdFALSE; BaseType_t xYieldRequired = pdFALSE;
#ifdef VERIFAST TCB_t * const pxTCB = xTaskToResume;
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
TCB_t * pxTCB = xTaskToResume;
#else
TCB_t * const pxTCB = xTaskToResume;
#endif /* VERIFAST */
UBaseType_t uxSavedInterruptStatus; UBaseType_t uxSavedInterruptStatus;
configASSERT( xTaskToResume ); configASSERT( xTaskToResume );
@ -4559,14 +4532,7 @@ void vTaskMissedYield( void )
UBaseType_t uxTaskGetTaskNumber( TaskHandle_t xTask ) UBaseType_t uxTaskGetTaskNumber( TaskHandle_t xTask )
{ {
UBaseType_t uxReturn; UBaseType_t uxReturn;
#ifdef VERIFAST TCB_t const * pxTCB;
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
TCB_t * pxTCB;
#else
TCB_t const * pxTCB;
#endif /* VERIFAST */
if( xTask != NULL ) if( xTask != NULL )
{ {
@ -5381,14 +5347,7 @@ static void prvResetNextTaskUnblockTime( void )
BaseType_t xTaskPriorityInherit( TaskHandle_t const pxMutexHolder ) BaseType_t xTaskPriorityInherit( TaskHandle_t const pxMutexHolder )
{ {
#ifdef VERIFAST TCB_t * const pxMutexHolderTCB = pxMutexHolder;
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
TCB_t * pxMutexHolderTCB = pxMutexHolder;
#else
TCB_t * const pxMutexHolderTCB = pxMutexHolder;
#endif /* VERIFAST */
BaseType_t xReturn = pdFALSE; BaseType_t xReturn = pdFALSE;
/* If the mutex was given back by an interrupt while the queue was /* If the mutex was given back by an interrupt while the queue was
@ -5566,14 +5525,7 @@ static void prvResetNextTaskUnblockTime( void )
void vTaskPriorityDisinheritAfterTimeout( TaskHandle_t const pxMutexHolder, void vTaskPriorityDisinheritAfterTimeout( TaskHandle_t const pxMutexHolder,
UBaseType_t uxHighestPriorityWaitingTask ) UBaseType_t uxHighestPriorityWaitingTask )
{ {
#ifdef VERIFAST TCB_t * const pxTCB = pxMutexHolder;
/* Reason for rewrite:
* VeriFast does not support const pointers.
*/
TCB_t * pxTCB = pxMutexHolder;
#else
TCB_t * const pxTCB = pxMutexHolder;
#endif /* VERIFAST */
UBaseType_t uxPriorityUsedOnEntry, uxPriorityToUse; UBaseType_t uxPriorityUsedOnEntry, uxPriorityToUse;
const UBaseType_t uxOnlyOneMutexHeld = ( UBaseType_t ) 1; const UBaseType_t uxOnlyOneMutexHeld = ( UBaseType_t ) 1;