From fa0c79015c3ecd2ad63dbf1b50f60039cf043151 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 17 Nov 2020 16:11:43 +0100
Subject: Builtin mem spec in scheduler and some needed proof in Postpasssch.v

---
 aarch64/PostpassSchedulingOracle.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'aarch64/PostpassSchedulingOracle.ml')

diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index 886519b2..821a1d53 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -462,7 +462,7 @@ let builtin_rec ef args res =
   (* XXX verify this *)
   {
     inst = builtin_real;
-    write_locs = [];
+    write_locs = [ Mem ];
     read_locs = [ Mem ];
     is_control = true;
   }
-- 
cgit