1 files changed, 22 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
new file mode 100644
index 000000000..5a79ae8cd
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
@@ -0,0 +1,22 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index df2b9c8c..c2265c26 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -105,7 +105,7 @@ static BaseType_t prvIsQueueFull( const Queue_t *pxQueue ) PRIVILEGED_FUNCTION;
+  * Copies an item into the queue, either at the front of the queue or the
+  * back of the queue.
+  */
+-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
+
+ /*
+  * Copies an item out of a queue.
+@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue;
+ #endif /* configUSE_MUTEXES */
+ /*-----------------------------------------------------------*/
+
+-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
+ {
+ BaseType_t xReturn = pdFALSE;
+ UBaseType_t uxMessagesWaiting;