From 230c196bfc825f66a2e1d96e57a4a38280fe80da Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Sat, 22 Oct 2016 13:35:06 +0100
Subject: fixes following interface changes (type of instruction, name of
 barrier)

---
 mips/mips_extras.lem                 | 2 +-
 src/lem_interp/run_with_elf.ml       | 6 +++---
 src/lem_interp/run_with_elf_cheri.ml | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index b4db9291..74119914 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -74,5 +74,5 @@ let memory_vals : memory_write_vals =
 
 let barrier_functions = [
   (*Need to know what barrier kind to install*)
-  ("MEM_sync", Isync);
+  ("MEM_sync", Barrier_Isync);
   ]
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 224f2860..b04911f1 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -883,14 +883,14 @@ let stop_condition_met model instr =
   match model with
   | PPC ->
     (match instr with
-     | ("Sc", [("Lev", _, arg)], []) ->
+     | ("Sc", [("Lev", _, arg)]) ->
        Nat_big_num.equal (integer_of_bit_list arg) (Nat_big_num.of_int 32)
      | _ -> false)
   | AArch64 -> (match instr with
-    | ("ImplementationDefinedStopFetching", _, _) -> true
+    | ("ImplementationDefinedStopFetching", _) -> true
     | _ -> false)
   | MIPS -> (match instr with 
-    | ("HCF", _, _) -> 
+    | ("HCF", _) -> 
       resultf "DEBUG MIPS PC %s\n"  (Printing_functions.logfile_register_value_to_string (Reg.find "PC" !reg));
       debug_print_gprs 0 31;
       true
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 71d173d8..19a62201 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -964,14 +964,14 @@ let stop_condition_met model instr =
   match model with
   | PPC ->
     (match instr with
-     | ("Sc", [("Lev", _, arg)], []) ->
+     | ("Sc", [("Lev", _, arg)]) ->
        Nat_big_num.equal (integer_of_bit_list arg) (Nat_big_num.of_int 32)
      | _ -> false)
   | AArch64 -> (match instr with
-    | ("ImplementationDefinedStopFetching", _, _) -> true
+    | ("ImplementationDefinedStopFetching", _) -> true
     | _ -> false)
   | MIPS -> (match instr with 
-    | ("HCF", _, _) -> 
+    | ("HCF", _) -> 
       resultf "DEBUG MIPS PC %s\n"  (Printing_functions.logfile_register_value_to_string (Reg.find "PC" !reg));
       debug_print_gprs 0 31;
       resultf "DEBUG CAP PCC %s\n"  (Printing_functions.logfile_register_value_to_string (Reg.find "PCC" !reg));
-- 
cgit v1.2.3