1#
2# Copyright 2014, General Dynamics C4 Systems
3#
4# SPDX-License-Identifier: GPL-2.0-only
5#
6
7## Targets
8images: BaseRefine CBaseRefine Refine CRefine
9default: images test
10test:
11all: images test
12report-regression:
13	@echo Refine Access CBaseRefine CRefine \
14	      DRefine InfoFlow InfoFlowCBase InfoFlowC DPolicy \
15		  DSpecProofs Bisim
16
17#
18# Setup heaps.
19#
20
21# Refine heaps.
22HEAPS += AInvs BaseRefine Refine RefineOrphanage
23
24# CRefine heaps.
25HEAPS += CKernel CSpec CBaseRefine CRefine
26
27# capDL heaps.
28HEAPS += DBaseRefine DRefine DPolicy SepDSpec DSpecProofs
29
30# Security Proofs
31HEAPS += Access InfoFlow InfoFlowCBase InfoFlowC
32
33# Binary Verification
34HEAPS += SimplExportAndRefine
35
36# Separation Kernel Bisimilarity
37HEAPS += Bisim
38
39# Separation Logic Tactics
40HEAPS += SepTactics
41
42# Additional dependencies
43
44BaseRefine Refine DBaseRefine DRefine: design-spec
45
46# CKernel uses the `machinety=machine_state` option for `install_C_file`,
47# and therefore depends on `design-spec`.
48CKernel CSpec : c-kernel design-spec
49
50CBaseRefine CRefine SimplExportAndRefine : c-kernel design-spec ASpec-files
51
52# Preprocess the kernel's source code and bitfield theory files.
53c-kernel: .FORCE
54	cd ../spec && $(ISABELLE_TOOL) env make c-kernel
55.PHONY: c-kernel
56
57# Run the haskell translator
58design-spec: .FORCE
59	cd ../spec && $(ISABELLE_TOOL) env make design-spec
60.PHONY: design-spec
61
62ASpec-files: .FORCE
63	cd ../spec && make ASpec-files
64.PHONY: ASpec-files
65
66include ../misc/isa-common.mk
67
68# SimplExport is treated specially, to not save an image.
69SimplExport: c-kernel design-spec
70	$(ISABELLE_TOOL) build -v -c -d $(ROOT_PATH) $@
71.PHONY: SimplExport
72