Update VeriFast proofs

.github/workflows/ci.yml

@@ -114,7 +114,7 @@ jobs:
           # Add path to the tool to the environment variable.
           PATH=$PATH:commonCI/spellings/tools
           # Make sure that only Amazon licenced files are checked.
-          sed -i 's/`find $DIRNAME \\( -iname \\\*\.\[ch\] -o -iname \\\*\.dox \\) -type f`/`grep -ril "copyright \(c\) \[0-9\]\[0-9\]\[0-9\]\[0-9\] amazon.com" | grep "\\.\[ch\]"`/g' commonCI/spellings/tools/find-unknown-comment-words
+          sed -i 's/`find $DIRNAME \\( -iname \\\*\.\[ch\] -o -iname \\\*\.dox \\) -type f`/`grep -ril "copyright \(c\) \[0-9\]\[0-9\]\[0-9\]\[0-9\] amazon.com" | grep "\\.\[ch\]" | grep -v "FreeRTOS\/FreeRTOS\/Test\/VeriFast"`/g' commonCI/spellings/tools/find-unknown-comment-words
           # Run the spell check script.
           find-unknown-comment-words --directory FreeRTOS/ --lexicon FreeRTOS/lexicon.txt
           # Check the exit status.

FreeRTOS/Test/VeriFast/Makefile

@@ -18,7 +18,7 @@ all: queue list
 
 .PHONY: queue
 queue:
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/create.c                    | $(call check_coverage,325)
+	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/create.c                    | $(call check_coverage,315)
 	@$(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)
@@ -41,26 +41,11 @@ queue:
 list:
 	@$(VERIFAST) $(VERIFAST_ARGS)                         list/listLIST_IS_EMPTY.c   | $(call check_coverage,314)
 	@$(VERIFAST) $(VERIFAST_ARGS)                         list/uxListRemove.c        | $(call check_coverage,440)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialise.c     | $(call check_coverage,325)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialise.c     | $(call check_coverage,329)
 	@$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialiseItem.c | $(call check_coverage,316)
 	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsertEnd.c      | $(call check_coverage,410)
 	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsert.c         | $(call check_coverage,456)
 
 .PHONY: proof_changes
 proof_changes:
 	@git grep "if[n]*def VERIFAST" | cut  -f 3- -d ' ' | sort | uniq
-
-GIT?=git
-NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel
-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)
-	@$(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_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_HEADER) include/list.h

FreeRTOS/Test/VeriFast/README.md

@@ -56,6 +56,7 @@ Then click `Verify` and `Verify Program` (or press F5). Note that the following
 proofs require arithmetic overflow checking to be turned off (click `Verify`
 and uncheck `Check arithmetic overflow`).
 
+  - `queue/create.c`
   - `queue/prvCopyDataToQueue.c`
   - `queue/xQueueGenericSendFromISR.c`
   - `queue/xQueueReceiveFromISR.c`

FreeRTOS/Test/VeriFast/docs/signoff.md

@@ -71,16 +71,19 @@ A side-by-side diff with respect to the source code can be generated. See
 The main queue changes are:
 
   - merge cTxLock and cRxLock critical regions: under approximate queue
-	unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
+    unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
     single critical region instead of two separate critical regions. In
-	practice, this is not an issue since no ISR function reads-from both
+    practice, this is not an issue since no ISR function reads-from both
     cTxLock and cRxLock.
   - model single malloc of struct and buffer: split the single malloc of the
     queue struct and storage into two separate mallocs.
   - xQueueGenericReset happens-before concurrent behavior: assume that queue
     initialisation is not concurrent.
   - do not model pxIndex and xListEnd of xLIST struct: ignore these fields in
-    the list structs of the queue implementation
+    the list structs of the queue implementation.
+  - we do not use the prvIncrementQueueTxLock or prvIncrementQueueRxLock macros
+    in xQueueGenericSendFromISR and xQueueReceiveFromISR functions.
+  - we prove an older version of xQueueGenericReset that always resets a queue
 
 The main list changes are:
 

FreeRTOS/Test/VeriFast/include/proof/common.gh

@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202112.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