diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/hol/sail2_prompt_monad.lem | 2 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem index ade12347..896c1a9c 100644 --- a/lib/hol/sail2_prompt_monad.lem +++ b/lib/hol/sail2_prompt_monad.lem @@ -44,7 +44,7 @@ let inline read_memt = read_memtS let inline read_mem = read_memS let inline excl_result = excl_resultS let inline write_reg = write_regS -let inline write_mem_ea wk addr sz = return () +let inline write_mem_ea wk addrsize addr sz = return () let inline write_memt = write_memtS let inline write_mem = write_memS let barrier _ = return () diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 8b189f7a..e8148597 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -91,7 +91,7 @@ lemma liftState_read_memt[liftState_simp]: split: option.splits intro: bindS_cong) lemma liftState_read_mem[liftState_simp]: - shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" + shows "liftState r (read_mem BCa BCb rk asz a sz) = read_memS BCa BCb rk a sz" by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def read_memtS_def prod.case_distrib option.case_distrib[where h = "liftState r"] @@ -100,7 +100,7 @@ lemma liftState_read_mem[liftState_simp]: lemma liftState_write_mem_ea_BC: assumes "unsigned_method BCa a = Some a'" - shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()" + shows "liftState r (write_mem_ea BCa rk asz a sz) = returnS ()" using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def) (*lemma liftState_write_mem_ea[liftState_simp]: @@ -118,7 +118,7 @@ lemma liftState_write_memt[liftState_simp]: by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits) lemma liftState_write_mem[liftState_simp]: - "liftState r (write_mem BCa BCv wk addr sz v) = write_memS BCa BCv wk addr sz v" + "liftState r (write_mem BCa BCv wk addrsize addr sz v) = write_memS BCa BCv wk addr sz v" by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp split: option.splits) |