diff options
| author | Robert Norton | 2016-10-22 13:35:06 +0100 |
|---|---|---|
| committer | Robert Norton | 2016-10-22 13:35:06 +0100 |
| commit | 230c196bfc825f66a2e1d96e57a4a38280fe80da (patch) | |
| tree | 9d558279b044bfd5c000ccffaea07aa1986788f8 | |
| parent | 208f1ea5626ac37ac0b1ac4a67a43d3c558d1e4d (diff) | |
fixes following interface changes (type of instruction, name of barrier)
| -rw-r--r-- | mips/mips_extras.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 6 | ||||
| -rw-r--r-- | 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)); |