github-forks
/
FreeRTOS
mirror of https://github.com/FreeRTOS/FreeRTOS.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Syntactic proof changes to track 10.4.1 changes (#322)

Browse Source 
All changes restricted to comments/formatting.
pull/328/head
Nathan Chong 4 years ago committed by GitHub
parent 8979b3817b
commit bc54c6bc10
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 19 additions and 17 deletions
Show Stats Download Patch File Download Diff File

10
FreeRTOS/Test/VeriFast/Makefile
Unescape Escape View File

@ -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

10
FreeRTOS/Test/VeriFast/list/vListInsert.c
Unescape Escape View File

@ -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.

2
FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
Unescape Escape View File

@ -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

6
FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
Unescape Escape View File

@ -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;

4
FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
Unescape Escape View File

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

4
FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
Unescape Escape View File

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

Write Preview
Loading…
Cancel
Save