From 80384aeee9482b481b7c1d23a3155098c5d90d28 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 4 Jun 2018 16:58:14 +0100
Subject: Fix bug with function return types in C backend

---
 aarch64/Makefile | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'aarch64')

diff --git a/aarch64/Makefile b/aarch64/Makefile
index 0ef6b0f0..e307f604 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -4,6 +4,12 @@ export SAIL_DIR
 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
+
+aarch64: no_vector.sail
+	$(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
+
 aarch64.lem: no_vector.sail
 	$(SAIL) $^ -o aarch64 -lem -lem_lib Aarch64_extras -memo_z3 -undefined_gen -no_lexp_bounds_check
 aarch64_types.lem: aarch64.lem
-- 
cgit v1.2.3