From 5309372245eff6da54e3baa708c9061c6c284299 Mon Sep 17 00:00:00 2001
From: Nathan Chong <52972368+nchong-at-aws@users.noreply.github.com>
Date: Thu, 25 Feb 2021 16:00:22 -0500
Subject: Minor VeriFast proof changes to match V10.4.3 (#519)

* Minor changes for V10.4.3

* Update license
---
 FreeRTOS/Test/VeriFast/Makefile                          | 10 +++++-----
 FreeRTOS/Test/VeriFast/include/proof/common.gh           |  6 +++++-
 FreeRTOS/Test/VeriFast/include/proof/list.h              |  6 +++++-
 FreeRTOS/Test/VeriFast/include/proof/queue.h             |  6 +++++-
 FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h    |  6 +++++-
 FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c          |  6 +++++-
 FreeRTOS/Test/VeriFast/list/uxListRemove.c               |  6 +++++-
 FreeRTOS/Test/VeriFast/list/vListInitialise.c            |  6 +++++-
 FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c        |  6 +++++-
 FreeRTOS/Test/VeriFast/list/vListInsert.c                |  6 +++++-
 FreeRTOS/Test/VeriFast/list/vListInsertEnd.c             |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/create.c                    |  9 ++++++++-
 FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c      |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c        |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c           |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c            |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/prvLockQueue.c              |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c            |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c    |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c    |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/vQueueDelete.c              |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c         |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c  |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c  |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueuePeek.c                |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c         |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueueReceive.c             |  6 +++++-
 FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c      |  6 +++++-
 29 files changed, 148 insertions(+), 33 deletions(-)

diff --git a/FreeRTOS/Test/VeriFast/Makefile b/FreeRTOS/Test/VeriFast/Makefile
index ba15befc7..bbbb541c3 100644
--- a/FreeRTOS/Test/VeriFast/Makefile
+++ b/FreeRTOS/Test/VeriFast/Makefile
@@ -18,7 +18,7 @@ all: queue list
 
 .PHONY: queue
 queue:
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/create.c                    | $(call check_coverage,324)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/create.c                    | $(call check_coverage,325)
 	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvCopyDataFromQueue.c      | $(call check_coverage,308)
 	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c        | $(call check_coverage,336)
 	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueEmpty.c           | $(call check_coverage,289)
@@ -52,10 +52,10 @@ proof_changes:
 
 GIT?=git
 NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel
-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
+NO_CHANGE_EXPECTED_HASH_QUEUE        = ec62f69dab7
+NO_CHANGE_EXPECTED_HASH_QUEUE_HEADER = ec62f69dab7
+NO_CHANGE_EXPECTED_HASH_LIST         = ec62f69dab7
+NO_CHANGE_EXPECTED_HASH_LIST_HEADER  = ec62f69dab7
 .PHONY: synced_with_source_check
 synced_with_source_check:
 	@rm -rf $(NO_CHANGE_CHECKOUT_DIR)
diff --git a/FreeRTOS/Test/VeriFast/include/proof/common.gh b/FreeRTOS/Test/VeriFast/include/proof/common.gh
index 430bad9d1..c4f8082de 100644
--- a/FreeRTOS/Test/VeriFast/include/proof/common.gh
+++ b/FreeRTOS/Test/VeriFast/include/proof/common.gh
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #ifndef COMMON_H
diff --git a/FreeRTOS/Test/VeriFast/include/proof/list.h b/FreeRTOS/Test/VeriFast/include/proof/list.h
index 1b80d3b07..c803b2c2c 100644
--- a/FreeRTOS/Test/VeriFast/include/proof/list.h
+++ b/FreeRTOS/Test/VeriFast/include/proof/list.h
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #ifndef LIST_H
diff --git a/FreeRTOS/Test/VeriFast/include/proof/queue.h b/FreeRTOS/Test/VeriFast/include/proof/queue.h
index b24c6dd31..a40d15e46 100644
--- a/FreeRTOS/Test/VeriFast/include/proof/queue.h
+++ b/FreeRTOS/Test/VeriFast/include/proof/queue.h
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #ifndef QUEUE_H
diff --git a/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h b/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h
index 8aa07de24..c48edf808 100644
--- a/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h
+++ b/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #ifndef QUEUECONTRACTS_H
diff --git a/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c b/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c
index 83749ede7..c1b0ef5fe 100644
--- a/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c
+++ b/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/list.h"
diff --git a/FreeRTOS/Test/VeriFast/list/uxListRemove.c b/FreeRTOS/Test/VeriFast/list/uxListRemove.c
index 82700c1d3..607bb64d1 100644
--- a/FreeRTOS/Test/VeriFast/list/uxListRemove.c
+++ b/FreeRTOS/Test/VeriFast/list/uxListRemove.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/list.h"
diff --git a/FreeRTOS/Test/VeriFast/list/vListInitialise.c b/FreeRTOS/Test/VeriFast/list/vListInitialise.c
index c6d016d56..73a46734d 100644
--- a/FreeRTOS/Test/VeriFast/list/vListInitialise.c
+++ b/FreeRTOS/Test/VeriFast/list/vListInitialise.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/list.h"
diff --git a/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c b/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c
index f86c82147..3e183ed73 100644
--- a/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c
+++ b/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/list.h"
diff --git a/FreeRTOS/Test/VeriFast/list/vListInsert.c b/FreeRTOS/Test/VeriFast/list/vListInsert.c
index 48eaddce0..f5a4e0bcf 100644
--- a/FreeRTOS/Test/VeriFast/list/vListInsert.c
+++ b/FreeRTOS/Test/VeriFast/list/vListInsert.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/list.h"
diff --git a/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c b/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c
index 451347913..92dc1a27d 100644
--- a/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c
+++ b/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/list.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/create.c b/FreeRTOS/Test/VeriFast/queue/create.c
index 848ce2469..87c97c277 100644
--- a/FreeRTOS/Test/VeriFast/queue/create.c
+++ b/FreeRTOS/Test/VeriFast/queue/create.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
@@ -212,6 +216,9 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength,
         /* Check for multiplication overflow. */
         configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
 
+        /* Check for addition overflow. */
+        configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) >  xQueueSizeInBytes );
+
 #ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */
         pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) );
 #else
diff --git a/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c b/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c
index 2c20de5f2..a898153ed 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvCopyDataFromQueue.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c b/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c
index c9a47c4a4..b05f000a8 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvCopyDataToQueue.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c b/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c
index 7caea7ccb..ab2cf8a46 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvIsQueueEmpty.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c b/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c
index 0f52e44a4..c5dee655f 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvIsQueueFull.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c b/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c
index 2fe774b74..64b626885 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvLockQueue.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
index d16fadc8c..f49ec684e 100644
--- a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
+++ b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c b/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c
index 809b67c6f..874a25316 100644
--- a/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c
+++ b/FreeRTOS/Test/VeriFast/queue/uxQueueMessagesWaiting.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c b/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c
index 265b3006b..3edba5416 100644
--- a/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c
+++ b/FreeRTOS/Test/VeriFast/queue/uxQueueSpacesAvailable.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c
index e80dee9be..41fc6c6b9 100644
--- a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c
+++ b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c
index c628f475e..de882a997 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
index 545ecf303..f922f66d2 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSendFromISR.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c
index 08d8117ab..6a0a9158f 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueEmptyFromISR.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c
index c8a3f419f..1b4024526 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c b/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c
index 7722bb72c..90f5ea875 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueuePeek.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
index 2fa081f07..deec0ac45 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueuePeekFromISR.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c b/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c
index 09a419de0..0eba2e5c7 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
index a69098c54..582c27aa4 100644
--- a/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
+++ b/FreeRTOS/Test/VeriFast/queue/xQueueReceiveFromISR.c
@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202012.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -18,6 +18,10 @@
  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ *
  */
 
 #include "proof/queue.h"
-- 
cgit v1.2.1