Skip to content
This repository has been archived by the owner on Dec 8, 2022. It is now read-only.

Change uxPendedTicks to xPendedTicks in all proofs #1758

Merged
merged 1 commit into from
Feb 14, 2020
Merged

Change uxPendedTicks to xPendedTicks in all proofs #1758

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions tools/cbmc/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,12 +65,15 @@ index ff657733..8b57d198 100644
PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */

#if( INCLUDE_vTaskDelete == 1 )
@@ -368,7 +368,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseTyp
@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseTyp

/* Other file private variables. --------------------------------*/
PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType_t ) 0U;
PRIVILEGED_DATA static volatile TickType_t xTickCount = ( TickType_t ) configINITIAL_TICK_COUNT;
PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority = tskIDLE_PRIORITY;
PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning = pdFALSE;
-PRIVILEGED_DATA static volatile UBaseType_t uxPendedTicks = ( UBaseType_t ) 0U;
+PRIVILEGED_DATA static UBaseType_t uxPendedTicks = ( UBaseType_t ) 0U;
-PRIVILEGED_DATA static volatile TickType_t xPendedTicks = ( TickType_t ) 0U;
+PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whitespace - should you run format?

PRIVILEGED_DATA static volatile BaseType_t xYieldPending = pdFALSE;
PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows = ( BaseType_t ) 0;
PRIVILEGED_DATA static UBaseType_t uxTaskNumber = ( UBaseType_t ) 0U;
8 changes: 4 additions & 4 deletions tools/cbmc/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,17 +6,17 @@ index 17a6964e..24a40c29 100644
* Checks to see if a queue is a member of a queue set, and if so, notifies
* the queue set that the queue contains data.
*/
- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition ) PRIVILEGED_FUNCTION;
+ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition ) PRIVILEGED_FUNCTION;
- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
+ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
#endif

/*
@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue;

#if ( configUSE_QUEUE_SETS == 1 )

- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition )
+ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition )
- static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
+ BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
{
Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer;
BaseType_t xReturn = pdFALSE;
4 changes: 2 additions & 2 deletions tools/cbmc/proofs/Queue/QueueGenericSend/QueueGenericSend_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueu
}
}
#else
BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition )
BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
{
Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer;
configASSERT( pxQueueSetContainer );
Expand All @@ -69,7 +69,7 @@ BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueu
configASSERT( pxQueue );
if( pxQueue->pxQueueSetContainer != NULL )
{
prvNotifyQueueSetContainer(pxQueue, queueSEND_TO_BACK);
prvNotifyQueueSetContainer(pxQueue);
}
listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) );
pxQueue->cTxLock = queueUNLOCKED;
Expand Down
2 changes: 1 addition & 1 deletion tools/cbmc/proofs/TaskPool/TaskDelay/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ This proof demonstrates the memory safety of the TaskDelay function. We assume
that `pxCurrentTCB` is initialized and inserted in one of the ready tasks lists
(with and without another task in the same list). We abstract function
`xTaskResumeAll` by assuming that `xPendingReadyList` is empty and
`uxPendedTicks` is `0`. Finally, we assume nondeterministic values for global
`xPendedTicks` is `0`. Finally, we assume nondeterministic values for global
variables `xTickCount` and `xNextTaskUnblockTime`, and `pdFALSE` for
`uxSchedulerSuspended` (to avoid assertion failure).

Expand Down
4 changes: 2 additions & 2 deletions tools/cbmc/proofs/TaskPool/TaskDelay/tasks_test_access_functions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ BaseType_t xPrepareTaskLists( void )
/*
* We stub out `xTaskResumeAll` including the assertion and change on
* variables `uxSchedulerSuspended`. We assume that `xPendingReadyList`
* is empty to avoid the first loop, and uxPendedTicks to avoid the second
* is empty to avoid the first loop, and xPendedTicks to avoid the second
* one. Finally, we return a nondeterministic value (overapproximation)
*/
BaseType_t xTaskResumeAllStub( void )
Expand All @@ -137,7 +137,7 @@ BaseType_t xTaskResumeAllStub( void )
{
--uxSchedulerSuspended;
__CPROVER_assert( listLIST_IS_EMPTY( &xPendingReadyList ), "Pending ready tasks list not empty." );
__CPROVER_assert( uxPendedTicks == 0 , "uxPendedTicks is not equal to zero.");
__CPROVER_assert( xPendedTicks == 0 , "xPendedTicks is not equal to zero.");
}
taskEXIT_CRITICAL();

Expand Down
2 changes: 1 addition & 1 deletion tools/cbmc/proofs/TaskPool/TaskIncrementTick/tasks_test_access_functions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ TaskHandle_t xUnconstrainedTCB( void )
*/
void vSetGlobalVariables()
{
uxPendedTicks = nondet_ubasetype();
xPendedTicks = nondet_ubasetype();
uxSchedulerSuspended = nondet_ubasetype();
xYieldPending = nondet_basetype();
xTickCount = nondet_ticktype();
Expand Down
2 changes: 1 addition & 1 deletion tools/cbmc/proofs/TaskPool/TaskResumeAll/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
This proof demonstrates the memory safety of the TaskResumeAll function. We
assume that task lists are initialized and filled with a few list items. We
also assume that some global variables are set to a nondeterministic value,
except for `uxSchedulerSuspended` which cannot be 0 and `uxPendedTicks` which
except for `uxSchedulerSuspended` which cannot be 0 and `xPendedTicks` which
is either `1` (to unwind a loop in a reasonable amount of time) or `0`.

Configurations available:
Expand Down
4 changes: 2 additions & 2 deletions tools/cbmc/proofs/TaskPool/TaskResumeAll/tasks_test_access_functions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ TaskHandle_t xUnconstrainedTCB( void )
}

/*
* We set uxPendedTicks since __CPROVER_assume does not work
* We set xPendedTicks since __CPROVER_assume does not work
* well with statically initialised variables
*/
void vSetGlobalVariables( void ) {
Expand All @@ -76,7 +76,7 @@ void vSetGlobalVariables( void ) {
__CPROVER_assume( uxNonZeroValue != 0 );

uxSchedulerSuspended = uxNonZeroValue;
uxPendedTicks = nondet_bool() ? PENDED_TICKS : 0;
xPendedTicks = nondet_bool() ? PENDED_TICKS : 0;
uxCurrentNumberOfTasks = nondet_ubasetype();
xTickCount = nondet_ticktype();
}
Expand Down