diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-08-13 15:41:48 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-08-13 15:41:48 +0100 |
| commit | 503cb6eca4831609e46abf22a54d4ba4b663d2b5 (patch) | |
| tree | cbdf09e763c4627295ae54aadfa92413518cf075 | |
| parent | eafbb796e16ac61ef39d36b32524b40ada195375 (diff) | |
| download | sail-riscv-503cb6eca4831609e46abf22a54d4ba4b663d2b5.zip sail-riscv-503cb6eca4831609e46abf22a54d4ba4b663d2b5.tar.gz sail-riscv-503cb6eca4831609e46abf22a54d4ba4b663d2b5.tar.bz2 | |
Fix Coq duopod build by giving missing termination measure
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | model/riscv_termination_duo.sail | 1 |
2 files changed, 2 insertions, 1 deletions
@@ -289,7 +289,7 @@ 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) -$(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail +$(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 $^ diff --git a/model/riscv_termination_duo.sail b/model/riscv_termination_duo.sail new file mode 100644 index 0000000..74ee253 --- /dev/null +++ b/model/riscv_termination_duo.sail @@ -0,0 +1 @@ +termination_measure n_leading_spaces s = string_length(s) |