Move forward Kernel submodule pointer (#218)

* Move forward Kernel submodule pointer
* Fixing patches for CBMC proofs
* Update proofs to assume cTxLock != 127
* Update proofs to assume cRxLock != 127

7 files changed, 40 insertions, 32 deletions

diff --git a/FreeRTOS-Plus/Test/CBMC/include/queue_init.h b/FreeRTOS-Plus/Test/CBMC/include/queue_init.h
index f05d18830..10b7e5607 100644
--- a/FreeRTOS-Plus/Test/CBMC/include/queue_init.h
+++ b/FreeRTOS-Plus/Test/CBMC/include/queue_init.h
@@ -43,6 +43,7 @@
 		if( xSet )
 		{
 			xSet->cTxLock = nondet_int8_t();
+			__CPROVER_assume(xSet->cTxLock != 127);
 			xSet->cRxLock = nondet_int8_t();
 			xSet->uxMessagesWaiting = nondet_UBaseType_t();
 			xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
@@ -73,6 +74,7 @@ QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound )
 		xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
 	if(xQueue){
 		xQueue->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cTxLock != 127);
 		xQueue->cRxLock = nondet_int8_t();
 		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
 		/* This is an invariant checked with a couple of asserts in the code base.
@@ -105,6 +107,7 @@ QueueHandle_t xUnconstrainedQueue( void ) {
 
 	if(xQueue){
 		xQueue->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cTxLock != 127);
 		xQueue->cRxLock = nondet_int8_t();
 		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
 		/* This is an invariant checked with a couple of asserts in the code base.
@@ -126,6 +129,7 @@ QueueHandle_t xUnconstrainedMutex( void ) {
 		xQueueCreateMutex(ucQueueType);
 	if(xQueue){
 		xQueue->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cTxLock != 127);
 		xQueue->cRxLock = nondet_int8_t();
 		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
 		/* This is an invariant checked with a couple of asserts in the code base.
diff --git a/FreeRTOS/Source b/FreeRTOS/Source
-Subproject 6199b72fbf57a7c5b3d7b195a3bd1446779314c
+Subproject 805b15a0224672bc89b2effffb7ab4c1debc732
diff --git a/FreeRTOS/Test/CBMC/include/queue_init.h b/FreeRTOS/Test/CBMC/include/queue_init.h
index f05d18830..1ec75cb48 100644
--- a/FreeRTOS/Test/CBMC/include/queue_init.h
+++ b/FreeRTOS/Test/CBMC/include/queue_init.h
@@ -43,6 +43,7 @@
 		if( xSet )
 		{
 			xSet->cTxLock = nondet_int8_t();
+			__CPROVER_assume(xSet->cTxLock != 127);
 			xSet->cRxLock = nondet_int8_t();
 			xSet->uxMessagesWaiting = nondet_UBaseType_t();
 			xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
@@ -73,7 +74,9 @@ QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound )
 		xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
 	if(xQueue){
 		xQueue->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cTxLock != 127);
 		xQueue->cRxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cRxLock != 127);
 		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
 		/* This is an invariant checked with a couple of asserts in the code base.
 		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
@@ -105,6 +108,7 @@ QueueHandle_t xUnconstrainedQueue( void ) {
 
 	if(xQueue){
 		xQueue->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cTxLock != 127);
 		xQueue->cRxLock = nondet_int8_t();
 		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
 		/* This is an invariant checked with a couple of asserts in the code base.
@@ -126,6 +130,7 @@ QueueHandle_t xUnconstrainedMutex( void ) {
 		xQueueCreateMutex(ucQueueType);
 	if(xQueue){
 		xQueue->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xQueue->cTxLock != 127);
 		xQueue->cRxLock = nondet_int8_t();
 		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
 		/* This is an invariant checked with a couple of asserts in the code base.
diff --git a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch
index 29cde0e77..7eb4870a0 100644
--- a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch
+++ b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch
@@ -45,35 +45,32 @@ diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c
 index ff657733..8b57d198 100644
 --- a/FreeRTOS/Source/tasks.c
 +++ b/FreeRTOS/Source/tasks.c
-@@ -331,7 +331,7 @@ typedef tskTCB TCB_t;
+@@ -335,7 +335,7 @@ typedef tskTCB TCB_t;
  
  /*lint -save -e956 A manual analysis and inspection has been used to determine
- which static variables must be declared volatile. */
+  * which static variables must be declared volatile. */
 -PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL;
 +PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL;
  
  /* Lists for ready and blocked tasks. --------------------
- xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but
-@@ -340,8 +340,8 @@ the static qualifier. */
- PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];/*< Prioritised ready tasks. */
- PRIVILEGED_DATA static List_t xDelayedTaskList1;						/*< Delayed tasks. */
- PRIVILEGED_DATA static List_t xDelayedTaskList2;						/*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */
--PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList;				/*< Points to the delayed task list currently being used. */
--PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList;		/*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
-+PRIVILEGED_DATA static List_t * pxDelayedTaskList;				/*< Points to the delayed task list currently being used. */
-+PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList;		/*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
- 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. */
+  * xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but
+@@ -344,8 +344,8 @@ PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL;
+ PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ]; /*< Prioritised ready tasks. */
+ PRIVILEGED_DATA static List_t xDelayedTaskList1;                         /*< Delayed tasks. */
+ PRIVILEGED_DATA static List_t xDelayedTaskList2;                         /*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */
+-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList;              /*< Points to the delayed task list currently being used. */
+-PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList;      /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
++PRIVILEGED_DATA static List_t * pxDelayedTaskList;              /*< Points to the delayed task list currently being used. */
++PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList;      /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
+ 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,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 TickType_t xPendedTicks 			= ( TickType_t ) 0U;
-+PRIVILEGED_DATA static TickType_t xPendedTicks 			= ( TickType_t ) 0U;
- 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;
+ #if ( INCLUDE_vTaskDelete == 1 )
+@@ -372,7 +372,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType
+ 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 TickType_t xPendedTicks = ( TickType_t ) 0U;
++PRIVILEGED_DATA static TickType_t xPendedTicks = ( TickType_t ) 0U;
+ 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;
diff --git a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch
index bcbd2b5cb..bb8e724d7 100644
--- a/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch
+++ b/FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch
@@ -12,11 +12,11 @@ index 17a6964e..24a40c29 100644
 
  /*
 @@ -2957,7 +2957,7 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue )
-
+ 
  #if ( configUSE_QUEUE_SETS == 1 )
-
--	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;
+ 
+-    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;
diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c
index e9575adab..46372c895 100644
--- a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c
@@ -61,6 +61,7 @@ QueueSetHandle_t xUnconstrainedQueueSet()
 	if( xSet )
 	{
 		xSet->cTxLock = nondet_int8_t();
+		__CPROVER_assume(xSet->cTxLock != 127);
 		xSet->cRxLock = nondet_int8_t();
 		xSet->uxMessagesWaiting = nondet_UBaseType_t();
 		xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c
index 1db424998..04fb98020 100644
--- a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/prvUnlockQueue_harness.c
@@ -62,6 +62,7 @@ QueueSetHandle_t xUnconstrainedQueueSet()
 	if( xSet )
 	{
 		xSet->cTxLock = nondet_int8_t();
+		__CPROVER_assume( xSet->cTxLock != 127 );
 		xSet->cRxLock = nondet_int8_t();
 		xSet->uxMessagesWaiting = nondet_UBaseType_t();
 		xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();