summaryrefslogtreecommitdiff
path: root/src/reporting_basic.ml
diff options
context:
space:
mode:
authorThomas Bauereiss2018-03-02 00:28:56 +0000
committerThomas Bauereiss2018-03-14 12:05:46 +0000
commitdfc417cea131f3e8bb033f3e25b24c94f909c809 (patch)
tree5e50e7841a1616a652836c493b696b49f7cc3a3d /src/reporting_basic.ml
parent5494cba73d75349785452ec882b65cae11e78d8a (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 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions