#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#

## Targets
images: BaseRefine CBaseRefine Refine CRefine
default: images test
test:
all: images test
report-regression:
	@echo Refine Access CBaseRefine CRefine \
	      DRefine InfoFlow InfoFlowC DPolicy \
		  DSpecProofs SepTacticsExamples

#
# Setup heaps.
#

# Refine heaps.
HEAPS += AInvs BaseRefine Refine

# CRefine heaps.
HEAPS += CBaseRefine CRefine

# capDL heaps.
HEAPS += DBaseRefine DRefine DPolicy DSpecProofs

# Security Proofs
HEAPS += Access InfoFlow InfoFlowC

# Separation Logic Tactics
HEAPS += SepTactics SepTacticsExamples

# Additional dependencies

CBaseRefine CRefine: c-kernel

# Preprocess the kernel's source code and bitfield theory files.
c-kernel: .FORCE
	cd ../spec && $(ISABELLE_TOOL) env make c-kernel
.PHONY: c-kernel

include ../misc/isa-common.mk