aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorBrian Campbell <Brian.Campbell@ed.ac.uk>2019-01-01 13:56:16 +0000
committerBrian Campbell <Brian.Campbell@ed.ac.uk>2019-01-02 13:12:17 +0000
commit2ee907495d64b11ff853a68d68929395fc38bc3b (patch)
treeed8633a4c832a3763ca4b7490d216028e65d69c7 /Makefile
parentdc6f48b574c4215e46b79612a01d0c203698e3f8 (diff)
downloadsail-riscv-2ee907495d64b11ff853a68d68929395fc38bc3b.zip
sail-riscv-2ee907495d64b11ff853a68d68929395fc38bc3b.tar.gz
sail-riscv-2ee907495d64b11ff853a68d68929395fc38bc3b.tar.bz2
Add termination measures to get patch-free Coq output
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 30eeee3..397ec4c 100644
--- a/Makefile
+++ b/Makefile
@@ -11,6 +11,7 @@ SAIL_OTHER_RVFI_SRCS = prelude.sail rvfi_dii.sail riscv_types.sail riscv_sys.sai
SAIL_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail
SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail
SAIL_RVFI_SRCS = $(SAIL_OTHER_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail
+SAIL_COQ_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_termination.sail riscv_analysis.sail
PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
@@ -160,8 +161,8 @@ COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail
riscv_coq: riscv.v riscv_types.v
-riscv.v riscv_types.v: $(SAIL_SRCS) Makefile
- $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_SRCS)
+riscv.v riscv_types.v: $(SAIL_COQ_SRCS) Makefile
+ $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS)
riscv_duopod.v riscv_duopod_types.v: prelude.sail riscv_duopod.sail
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv_duopod -coq_lib riscv_extras $^
%.vo: %.v