diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/Makefile')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/Makefile | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/FreeRTOS/Test/VeriFast/Makefile b/FreeRTOS/Test/VeriFast/Makefile index bbbb541c3..476a6721c 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,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,7 +41,7 @@ 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) @@ -49,18 +49,3 @@ list: .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 |