ktest-hacked.mak

# CHANGE FROM ORIGINAL: corrected, path to krun, same depth as path to the original ktest.mak
MAKEFILE_PATH := $(dir $(abspath $(shell which krun)))

# path to the kompile binary of this distribuition
KOMPILE=$(abspath $(MAKEFILE_PATH)/../bin/kompile)
# ditto for krun
KRUN=$(abspath $(MAKEFILE_PATH)/../bin/krun)
# and kdep
KDEP=$(abspath $(MAKEFILE_PATH)/../bin/kdep)
# and kprove
KPROVE=$(abspath $(MAKEFILE_PATH)/../bin/kprove)
# path relative to current definition of test programs
TESTDIR?=tests
# path to put -kompiled directory in
DEFDIR?=.
# path relative to current definition of output/input files
RESULTDIR?=$(TESTDIR)
# all tests in test directory with matching file extension

# CHANGE FROM ORIGINAL: minor extension here to allow rewriting the var in Makefile
TESTS?=$(wildcard $(TESTDIR)/*.$(EXT))

PROOF_TESTS=$(wildcard $(TESTDIR)/*-spec.k)

CHECK=| diff -

.PHONY: kompile krun all clean update-results proofs

# run all tests
all: kompile krun proofs

# run only kompile
kompile: $(DEFDIR)/$(DEF)-kompiled/timestamp

$(DEFDIR)/%-kompiled/timestamp: %.k
	$(KOMPILE) $(KOMPILE_FLAGS) $(DEBUG) $< -d $(DEFDIR)
krun: $(TESTS)

proofs: $(PROOF_TESTS)

# run all tests and regenerate output files
update-results: krun proofs
update-results: CHECK=>

# run a single test. older versions of make run pattern rules in order, so
# if some programs should be run with different options their rule should be
# specified in the makefile prior to including ktest.mak.
%.$(EXT): kompile
ifeq ($(TESTDIR),$(RESULTDIR))
	cat $@.in 2>/dev/null | $(KRUN) $@ $(KRUN_FLAGS) $(DEBUG) -d $(DEFDIR) $(CHECK) $@.out
else
	cat $(RESULTDIR)/$(notdir $@).in 2>/dev/null | $(KRUN) $@ $(KRUN_FLAGS) $(DEBUG) -d $(DEFDIR) $(CHECK) $(RESULTDIR)/$(notdir $@).out
endif

%-spec.k: kompile
	$(KPROVE) -d $(DEFDIR) --z3-executable $@ $(CHECK) $@.out

clean:
	rm -rf $(DEFDIR)/$(DEF)-kompiled

.depend:
	@$(KDEP) $(DEF).k > .depend-tmp
	@mv .depend-tmp .depend

-include .depend