summaryrefslogtreecommitdiff
path: root/aarch64_small
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-06-04 17:36:22 +0100
committerAlasdair Armstrong2019-06-04 17:36:22 +0100
commit37c5fb51e9986917a791de73435e182549e21fca (patch)
treef6bd9bd26d80e51cf197b9ea8a5c9d5c3c61ec8b /aarch64_small
parent239e13dc149af80f979ea95a3c9b42220481a0a1 (diff)
Make sure aarch64_small can generate Jib for SMT
Add a test case for this
Diffstat (limited to 'aarch64_small')
-rw-r--r--aarch64_small/Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile
index fe4c5841..c1751a45 100644
--- a/aarch64_small/Makefile
+++ b/aarch64_small/Makefile
@@ -23,6 +23,9 @@ armV8.lem: $(SOURCES)
# also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem
$(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^
+smt: $(SOURCES)
+ $(SAIL) $(SAILFLAGS) -smt $^
+
for-rmem/armV8.lem: $(SOURCES)
mkdir -p $(dir $@)
# We do not need the isabelle .thy files, but sail always generates them