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