begriffs open source - cmsis-freertos/blob - Test/VeriFast/Makefile

   1 VERIFAST ?= verifast
   2 VERIFAST_ARGS = -I include -c $(EXTRA_VERIFAST_ARGS)
   3
   4 ifeq ($(NO_COVERAGE), 1)
   5 check_coverage = cat
   6 else
   7 check_coverage = perl -pe \
   8   'END { \
   9       if ($$status) { \
  10         print "Coverage regression failed: Expected $1 statements verified.\n"; \
  11       } \
  12       exit $$status; \
  13    } \
  14    $$status=/$1 statements verified/ ? 0 : 1;'
  15 endif
  16
  17 all: queue list
  18
  19 .PHONY: queue
  20 queue:
  21         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/create.c                    | $(call check_coverage,325)
  22         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvCopyDataFromQueue.c      | $(call check_coverage,308)
  23         @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c        | $(call check_coverage,336)
  24         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueEmpty.c           | $(call check_coverage,289)
  25         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueFull.c            | $(call check_coverage,289)
  26         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvLockQueue.c              | $(call check_coverage,290)
  27         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvUnlockQueue.c            | $(call check_coverage,304)
  28         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/uxQueueMessagesWaiting.c    | $(call check_coverage,292)
  29         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/uxQueueSpacesAvailable.c    | $(call check_coverage,290)
  30         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/vQueueDelete.c              | $(call check_coverage,287)
  31         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueGenericSend.c         | $(call check_coverage,335)
  32         @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueGenericSendFromISR.c  | $(call check_coverage,317)
  33         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueIsQueueEmptyFromISR.c | $(call check_coverage,287)
  34         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueIsQueueFullFromISR.c  | $(call check_coverage,287)
  35         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueuePeek.c                | $(call check_coverage,335)
  36         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueuePeekFromISR.c         | $(call check_coverage,300)
  37         @$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueReceive.c             | $(call check_coverage,337)
  38         @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueReceiveFromISR.c      | $(call check_coverage,314)
  39
  40 .PHONY: list
  41 list:
  42         @$(VERIFAST) $(VERIFAST_ARGS)                         list/listLIST_IS_EMPTY.c   | $(call check_coverage,314)
  43         @$(VERIFAST) $(VERIFAST_ARGS)                         list/uxListRemove.c        | $(call check_coverage,440)
  44         @$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialise.c     | $(call check_coverage,325)
  45         @$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialiseItem.c | $(call check_coverage,316)
  46         @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsertEnd.c      | $(call check_coverage,410)
  47         @$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsert.c         | $(call check_coverage,456)
  48
  49 .PHONY: proof_changes
  50 proof_changes:
  51         @git grep "if[n]*def VERIFAST" | cut  -f 3- -d ' ' | sort | uniq
  52
  53 GIT?=git
  54 NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel
  55 NO_CHANGE_EXPECTED_HASH_QUEUE        = ec62f69dab7
  56 NO_CHANGE_EXPECTED_HASH_QUEUE_HEADER = ec62f69dab7
  57 NO_CHANGE_EXPECTED_HASH_LIST         = ec62f69dab7
  58 NO_CHANGE_EXPECTED_HASH_LIST_HEADER  = ec62f69dab7
  59 .PHONY: synced_with_source_check
  60 synced_with_source_check:
  61         @rm -rf $(NO_CHANGE_CHECKOUT_DIR)
  62         @$(GIT) clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git $(NO_CHANGE_CHECKOUT_DIR)
  63         @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) queue.c
  64         @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE_HEADER) include/queue.h
  65         @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) list.c
  66         @cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST_HEADER) include/list.h