diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 95d25336..5b27bf1a 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1153,7 +1153,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = reg := Reg.add "nextPC" npc_reg !reg; | Some 1 -> reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; - | None -> failwith "invalid value of inBranchDelay"); + | _ -> failwith "invalid value of inBranchDelay"); let opcode = Opcode (get_opcode pc) in let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with | Instr(instruction,istate) -> diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index 0b563b27..5eb560e1 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1244,7 +1244,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = | Some 1 -> reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; - | None -> failwith "invalid value of inBranchDelay"); + | _ -> failwith "invalid value of inBranchDelay"); let opcode = Opcode (get_opcode pc) in let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with | Instr(instruction,istate) -> |