diff options
| author | Thomas Bauereiss | 2018-03-02 00:28:56 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-03-14 12:05:46 +0000 |
| commit | dfc417cea131f3e8bb033f3e25b24c94f909c809 (patch) | |
| tree | 5e50e7841a1616a652836c493b696b49f7cc3a3d /lib/isabelle/State_monad_lemmas.thy | |
| parent | 5494cba73d75349785452ec882b65cae11e78d8a (diff) | |
Add address to Write_tag outcome
The state monad currently assumes that tags are written to and read from
properly aligned addresses (since it does not know the capability size used in
the Sail model). This change allows the Sail model to pass in the aligned
address(es) even if data is written to an unaligned address. There might be
better ways to model tag writing, but this approach seems rather general.
Diffstat (limited to 'lib/isabelle/State_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index 746fd315..291157f5 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -274,7 +274,7 @@ lemma no_throw_mem_builtins: "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s" "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" - "\<And>t s. ignore_throw (write_tagS t) s = write_tagS t s" + "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s" "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def |