From bc54c6bc10bae9c1ad8334f2ea81329c8718da4d Mon Sep 17 00:00:00 2001
From: Nathan Chong <52972368+nchong-at-aws@users.noreply.github.com>
Date: Tue, 6 Oct 2020 16:17:29 -0400
Subject: [PATCH] Syntactic proof changes to track 10.4.1 changes (#322)
All changes restricted to comments/formatting.
---
FreeRTOS/Test/VeriFast/Makefile | 10 ++++++----
FreeRTOS/Test/VeriFast/list/vListInsert.c | 10 +++++-----
FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c | 2 +-
.../Test/VeriFast/queue/xQueueGenericSendFromISR.c | 6 +++---
FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c | 4 ++--
FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c | 4 ++--
6 files changed, 19 insertions(+), 17 deletions(-)
diff --git a/FreeRTOS/Test/VeriFast/Makefile b/FreeRTOS/Test/VeriFast/Makefile
index 3d9fb48002..ba15befc76 100644
--- a/FreeRTOS/Test/VeriFast/Makefile
+++ b/FreeRTOS/Test/VeriFast/Makefile
@@ -52,13 +52,15 @@ proof_changes:
GIT?=git
NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel
-NO_CHANGE_EXPECTED_HASH_QUEUE=587a83d6476
-NO_CHANGE_EXPECTED_HASH_LIST=bb1c4293787
+NO_CHANGE_EXPECTED_HASH_QUEUE = 3604527e3b3
+NO_CHANGE_EXPECTED_HASH_QUEUE_HEADER = d428209d018
+NO_CHANGE_EXPECTED_HASH_LIST = 3604527e3b3
+NO_CHANGE_EXPECTED_HASH_LIST_HEADER = 3604527e3b3
.PHONY: synced_with_source_check
synced_with_source_check:
@rm -rf $(NO_CHANGE_CHECKOUT_DIR)
@$(GIT) clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git $(NO_CHANGE_CHECKOUT_DIR)
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) queue.c
- @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) include/queue.h
+ @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE_HEADER) include/queue.h
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) list.c
- @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) include/list.h
+ @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST_HEADER) include/list.h
diff --git a/FreeRTOS/Test/VeriFast/list/vListInsert.c b/FreeRTOS/Test/VeriFast/list/vListInsert.c
index 96e333832e..bd1295a1e2 100644
--- a/FreeRTOS/Test/VeriFast/list/vListInsert.c
+++ b/FreeRTOS/Test/VeriFast/list/vListInsert.c
@@ -84,18 +84,18 @@ void vListInsert( List_t * const pxList,
{
/* *** NOTE ***********************************************************
* If you find your application is crashing here then likely causes are
- * listed below. In addition see https://www.freertos.org/FAQHelp.html for
+ * listed below. In addition see https://www.FreeRTOS.org/FAQHelp.html for
* more tips, and ensure configASSERT() is defined!
- * https://www.freertos.org/a00110.html#configASSERT
+ * https://www.FreeRTOS.org/a00110.html#configASSERT
*
* 1) Stack overflow -
- * see https://www.freertos.org/Stacks-and-stack-overflow-checking.html
+ * see https://www.FreeRTOS.org/Stacks-and-stack-overflow-checking.html
* 2) Incorrect interrupt priority assignment, especially on Cortex-M
* parts where numerically high priority values denote low actual
* interrupt priorities, which can seem counter intuitive. See
- * https://www.freertos.org/RTOS-Cortex-M3-M4.html and the definition
+ * https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html and the definition
* of configMAX_SYSCALL_INTERRUPT_PRIORITY on
- * https://www.freertos.org/a00110.html
+ * https://www.FreeRTOS.org/a00110.html
* 3) Calling an API function from within a critical section or when
* the scheduler is suspended, or calling an API function that does
* not end in "FromISR" from an interrupt.
diff --git a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
index 079573b2f9..92826bcea0 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
@@ -78,7 +78,7 @@ static void prvUnlockQueue( Queue_t * const pxQueue )
if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
{
/* The task waiting has a higher priority so record that a
- * context switch is required. */
+ * context switch is required. */
vTaskMissedYield();
}
else
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
index 2baa7e5e8b..a6bb2b2819 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
@@ -60,10 +60,10 @@ BaseType_t xQueueGenericSendFromISR( QueueHandle_t xQueue,
* assigned a priority above the configured maximum system call priority.
* Only FreeRTOS functions that end in FromISR can be called from interrupts
* that have been assigned a priority at or (logically) below the maximum
- * system call interrupt priority. FreeRTOS maintains a separate interrupt
+ * system call interrupt priority. FreeRTOS maintains a separate interrupt
* safe API to ensure interrupt entry is as fast and as simple as possible.
* More information (albeit Cortex-M specific) is provided on the following
- * link: http://www.freertos.org/RTOS-Cortex-M3-M4.html */
+ * link: https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html */
portASSERT_IF_INTERRUPT_PRIORITY_INVALID();
/* Similar to xQueueGenericSend, except without blocking if there is no room
@@ -164,7 +164,7 @@ BaseType_t xQueueGenericSendFromISR( QueueHandle_t xQueue,
if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
{
/* The task waiting has a higher priority so record that a
- * context switch is required. */
+ * context switch is required. */
if( pxHigherPriorityTaskWoken != NULL )
{
*pxHigherPriorityTaskWoken = pdTRUE;
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
index 0eb22ce62c..f41702087e 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
@@ -53,10 +53,10 @@ BaseType_t xQueuePeekFromISR( QueueHandle_t xQueue,
* assigned a priority above the configured maximum system call priority.
* Only FreeRTOS functions that end in FromISR can be called from interrupts
* that have been assigned a priority at or (logically) below the maximum
- * system call interrupt priority. FreeRTOS maintains a separate interrupt
+ * system call interrupt priority. FreeRTOS maintains a separate interrupt
* safe API to ensure interrupt entry is as fast and as simple as possible.
* More information (albeit Cortex-M specific) is provided on the following
- * link: http://www.freertos.org/RTOS-Cortex-M3-M4.html */
+ * link: https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html */
portASSERT_IF_INTERRUPT_PRIORITY_INVALID();
uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR();
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
index 0af8f8e301..658793609d 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
@@ -54,10 +54,10 @@ BaseType_t xQueueReceiveFromISR( QueueHandle_t xQueue,
* assigned a priority above the configured maximum system call priority.
* Only FreeRTOS functions that end in FromISR can be called from interrupts
* that have been assigned a priority at or (logically) below the maximum
- * system call interrupt priority. FreeRTOS maintains a separate interrupt
+ * system call interrupt priority. FreeRTOS maintains a separate interrupt
* safe API to ensure interrupt entry is as fast and as simple as possible.
* More information (albeit Cortex-M specific) is provided on the following
- * link: http://www.freertos.org/RTOS-Cortex-M3-M4.html */
+ * link: https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html */
portASSERT_IF_INTERRUPT_PRIORITY_INVALID();
uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR();