1# 2# Copyright 2014, NICTA 3# 4# This software may be distributed and modified according to the terms of 5# the BSD 2-Clause license. Note that NO WARRANTY is provided. 6# See "LICENSE_BSD2.txt" for details. 7# 8# @TAG(NICTA_BSD) 9# 10 11default: AutoCorresTest 12 13all: AutoCorres AutoCorresTest AutoCorresSEL4 AutoCorresDoc 14 15report-regression: 16 @echo AutoCorres AutoCorresTest AutoCorresDoc AutoCorresSEL4 17 18# Generate an Isabelle "ROOT" file containing all of our test cases. 19tests/ROOT: \ 20 tests/parse-tests tests/examples \ 21 tests/parse-tests/*.c \ 22 $(patsubst %.c,%.thy,$(wildcard tests/parse-tests/*.c)) \ 23 tests/proof-tests/*.c \ 24 tests/proof-tests/*.thy \ 25 tests/examples/*.c \ 26 tests/examples/*.thy \ 27 ../../misc/scripts/gen_isabelle_root.py 28 python ../../misc/scripts/gen_isabelle_root.py -o $@ -b AutoCorres -s AutoCorresTest -d HOL-Number_Theory \ 29 -i tests/parse-tests -i tests/proof-tests -i tests/examples --quick-and-dirty 30 31# Generate a Isabelle "All.thy" file containing imports to all the test cases. 32tests/All.thy: \ 33 tests/parse-tests tests/examples \ 34 tests/parse-tests/*.c \ 35 $(patsubst %.c,%.thy,$(wildcard tests/parse-tests/*.c)) \ 36 tests/proof-tests/*.c \ 37 tests/proof-tests/*.thy \ 38 tests/examples/*.c \ 39 tests/examples/*.thy \ 40 ../../misc/scripts/gen_isabelle_root.py 41 python ../../misc/scripts/gen_isabelle_root.py -T -o $@ \ 42 -i tests/parse-tests -i tests/proof-tests -i tests/examples 43 44# Generate a template ".thy" file from a ".c" file. 45%.thy: %.c 46 @echo "Generating '$@' from '$<'..." 47 @printf '(* @LICENSE(NICTA) *)\n\n' > $@ 48 @printf 'theory %s\nimports "AutoCorres.AutoCorres"\nbegin\n\n' $(notdir $(basename $<)) > $@ 49 @printf 'external_file "%s"\n\n' $(notdir $<) >> $@ 50 @printf 'install_C_file "%s"\n\n' $(notdir $<) >> $@ 51 @printf 'autocorres "%s"\n\n' $(notdir $<) >> $@ 52 @printf 'end\n' >> $@ 53 54# Test all the files in our "tests/" directory. 55AutoCorresTest: clean-tests tests/ROOT 56 $(ISABELLE_TOOL) build -d ../.. -d tests -b -v AutoCorresTest 57.PHONY: AutoCorresTest 58 59# Parse the seL4 kernel 60AutoCorresSEL4: 61 make -C ../../proof CBaseRefine 62 $(ISABELLE_TOOL) build -d ../.. -b -v AutoCorresSEL4 63.PHONY: AutoCorresSEL4 64 65# Build the documentation sub-sessions. 66AutoCorresDoc: 67 $(ISABELLE_TOOL) build -d ../.. -D doc/quickstart 68 69# Clean out files generated by the test suite. 70clean-tests: 71 rm -f tests/parse-tests/*.thy 72 rm -f tests/ROOT 73.PHONY: clean-tests 74 75clean: clean-tests 76 77HEAPS := AutoCorres 78 79include ../../misc/isa-common.mk 80 81