diff options
| author | Christopher Pulte | 2016-10-22 20:32:54 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-10-22 20:32:54 +0100 |
| commit | 0dbcb0e5653ea66c80daef1364de6fb2f5921186 (patch) | |
| tree | 4a885e591eaad5b562be5604c2f5a5b991a89945 /src/lem_interp | |
| parent | 72e9e83410ec1540c1993184a105696db4fba412 (diff) | |
| parent | 230c196bfc825f66a2e1d96e57a4a38280fe80da (diff) | |
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail
Diffstat (limited to 'src/lem_interp')
| -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)); |