summaryrefslogtreecommitdiff
path: root/mips/Makefile
diff options
context:
space:
mode:
authorBrian Campbell2018-05-04 19:08:15 +0100
committerBrian Campbell2018-05-04 19:08:15 +0100
commit05a4a75d328d3bd8469167f6f23dda918146117a (patch)
tree8d4175596391d22c9be89443f83e39ace9473896 /mips/Makefile
parent066ecac9d79769e1a759f8ed1b13b18548aef36c (diff)
Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERI
Diffstat (limited to 'mips/Makefile')
-rw-r--r--mips/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/mips/Makefile b/mips/Makefile
index 00703f62..a6a5bbdf 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -21,7 +21,7 @@ mips_no_tlb_types.lem: mips_no_tlb.lem
# TODO: Use monomorphisation so that we can switch to machine words
mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
- $(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+ $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
mips_types.lem: mips.lem
M%.thy: m%.lem m%_types.lem mips_extras.lem