diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 6 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 6 |
2 files changed, 6 insertions, 6 deletions
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)); |