From d91841f80740b210c673d3138f77b9d4d5684102 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 2 Nov 2017 14:06:24 +0000
Subject: reset inCCallDelay in code that is not dead.

---
 src/lem_interp/run_with_elf_cheri.ml    | 1 +
 src/lem_interp/run_with_elf_cheri128.ml | 1 +
 2 files changed, 2 insertions(+)

(limited to 'src')

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;
-- 
cgit v1.2.3