Reverted manual rewrites involving const pointers. Automatic rewrites are in place.

This commit is contained in:
Tobias Reinhard 2022-11-13 14:52:14 -05:00
parent a470fec6d0
commit a7fdaca373

25
tasks.c
View file

@ -2194,10 +2194,9 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
eTaskState eReturn; eTaskState eReturn;
#ifdef VERIFAST #ifdef VERIFAST
/* Reason for rewrite: /* Reason for rewrite:
* VeriFast does not support the following: * VeriFast does not support multiple pointer declarations to
* - const pointers * user-defined types in single statement (i.e., `A p1, p2;` is ok,
* - multiple pointer declarations to user-defined types in single * `A *p1, *p2;` fails)
* statement (i.e., `A p1, p2;` is ok, `A *p1, *p2;` fails)
*/ */
List_t const * pxStateList; List_t const * pxStateList;
List_t const * pxDelayedList; List_t const * pxDelayedList;
@ -2802,14 +2801,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
void vTaskResume( TaskHandle_t xTaskToResume ) void vTaskResume( TaskHandle_t xTaskToResume )
{ {
#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 */
/* It does not make sense to resume the calling task. */ /* It does not make sense to resume the calling task. */
configASSERT( xTaskToResume ); configASSERT( xTaskToResume );
@ -5432,14 +5424,7 @@ static void prvResetNextTaskUnblockTime( void )
BaseType_t xTaskPriorityDisinherit( TaskHandle_t const pxMutexHolder ) BaseType_t xTaskPriorityDisinherit( TaskHandle_t const pxMutexHolder )
{ {
#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 */
BaseType_t xReturn = pdFALSE; BaseType_t xReturn = pdFALSE;
if( pxMutexHolder != NULL ) if( pxMutexHolder != NULL )