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

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.

FreeRTOS/Source

@@ -1 +1 @@
-Subproject commit 6199b72fbf57a7c5b3d7b195a3bd1446779314cd
+Subproject commit 805b15a0224672bc89b2effffb7ab4c1debc7325

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.

FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch

@@ -45,17 +45,17 @@ 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. */
+  * 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. */
@@ -64,11 +64,8 @@ index ff657733..8b57d198 100644
 +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;
+ #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;

FreeRTOS/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch

@@ -18,5 +18,5 @@ index 17a6964e..24a40c29 100644
 -    static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
 +    BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
      {
- 	Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer;
+         Queue_t * pxQueueSetContainer = pxQueue->pxQueueSetContainer;
          BaseType_t xReturn = pdFALSE;

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();

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();