diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-10-07 16:00:56 +0100 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-10-09 22:04:15 -0700 |
| commit | 0e42c867fba498746405d2b878a12fd4d143c5d8 (patch) | |
| tree | 689e0ee412b6c91bcadb989148b72ad48b464a9b /Makefile | |
| parent | a13c0a435804a9a8250054c2e9af2eacfa883164 (diff) | |
| download | sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.zip sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.tar.gz sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.tar.bz2 | |
Add {read,write}_ram for Coq
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -288,22 +288,22 @@ riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile mkdir -p generated_definitions/coq/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS) + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras -coq_lib mem_metadata $(SAIL_COQ_SRCS) $(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail model/riscv_termination_duo.sail mkdir -p generated_definitions/coq/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras $^ + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras -coq_lib mem_metadata $^ %.vo: %.v ifeq ($(wildcard $(BBV_DIR)/theories),) - $(error BBV directory not found. Please set the BBV_DIR environment variable) + $(error BBV directory not found. Please set the BBV_DIR environment variable) endif ifeq ($(wildcard $(SAIL_LIB_DIR)/coq),) $(error lib directory of Sail not found. Please set the SAIL_LIB_DIR environment variable) endif coqc $(COQ_LIBS) $< -generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo -generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(ARCH)/riscv_duopod_types.vo handwritten_support/riscv_extras.vo +generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo +generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(ARCH)/riscv_duopod_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo echo_rmem_srcs: echo $(SAIL_RMEM_SRCS) @@ -363,4 +363,5 @@ clean: -rm -f z3_problems -Holmake cleanAll -rm -f handwritten_support/riscv_extras.vo handwritten_support/riscv_extras.glob handwritten_support/.riscv_extras.aux + -rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux ocamlbuild -clean |