diff options
| author | Alasdair Armstrong | 2018-12-20 22:00:40 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-20 22:00:40 +0000 |
| commit | 0a9200153430f5e727b3ebe1fa272d4842069530 (patch) | |
| tree | dff86bfcd0dd86879df00f82d4e6c6efb5a5d7b3 /aarch64/Makefile | |
| parent | 40f7f5d00a9afff27f1d2329ab525705e57c6d6f (diff) | |
Fix monomorpisation tests with typechecker changes
Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues
Diffstat (limited to 'aarch64/Makefile')
| -rw-r--r-- | aarch64/Makefile | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile index aa4d5301..365e23bd 100644 --- a/aarch64/Makefile +++ b/aarch64/Makefile @@ -5,13 +5,13 @@ SAIL_LIB_DIR:=$(SAIL_DIR)/lib SAIL:=$(SAIL_DIR)/sail aarch64.c: no_vector.sail - $(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c + $(SAIL) $(SAIL_FLAGS) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c aarch64_c: aarch64.c gcc -O2 $^ -o aarch64_c -lgmp -I $(SAIL_DIR)/lib aarch64: no_vector.sail - $(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 + $(SAIL) $(SAIL_FLAGS) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 aarch64_full: full.sail $(SAIL) $^ -o aarch64_full -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 @@ -23,5 +23,11 @@ aarch64_types.lem: aarch64.lem Aarch64.thy: aarch64_extras.lem aarch64_types.lem aarch64.lem lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^ +clean: + rm -rf _sbuild/ + rm -f aarch64 + rm -f aarch64.c + rm -f aarch64.lem + LOC_FILES:=prelude.sail full/spec.sail decode_start.sail full/decode.sail decode_end.sail main.sail include ../etc/loc.mk |