diff options
| author | Robert Norton | 2017-11-02 14:06:24 +0000 |
|---|---|---|
| committer | Robert Norton | 2017-11-02 14:06:24 +0000 |
| commit | d91841f80740b210c673d3138f77b9d4d5684102 (patch) | |
| tree | a44759fa1c902543afbc88150fb2a018c3c5142b /src | |
| parent | 40a85677707395199a005c2742304b80be87e117 (diff) | |
reset inCCallDelay in code that is not dead.
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 1 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index b50cb01d..8f7d5505 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1285,6 +1285,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = let npc_addr = add_address_nat pc_val 4 in let npc_reg = register_value_of_address npc_addr Sail_impl_base.D_decreasing in reg := Reg.add "nextPC" npc_reg !reg; + reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; | Some 1 -> reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 148b29ae..311d6f69 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1285,6 +1285,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = let npc_addr = add_address_nat pc_val 4 in let npc_reg = register_value_of_address npc_addr Sail_impl_base.D_decreasing in reg := Reg.add "nextPC" npc_reg !reg; + reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; | Some 1 -> reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; |