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