diff options
| author | Robert Norton | 2016-07-26 17:54:35 +0100 |
|---|---|---|
| committer | Robert Norton | 2016-07-26 17:54:35 +0100 |
| commit | 8e208dded40b6faeb69e8ddbf5bda3ed0c1e4194 (patch) | |
| tree | 1686512bab1409847574af0da35440c131955ef9 /src | |
| parent | e1fad3835b0864cce72abf548611581ae912a1a3 (diff) | |
Fix incomplete match warning in run_with*
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) -> |