diff options
| author | Christopher Pulte | 2019-03-02 11:36:45 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2019-03-02 11:36:45 +0000 |
| commit | 8e7138cded140de550cbb4d4f803d13d175b2d95 (patch) | |
| tree | 53aa35412fb6f1cb9c671f25dc1de63107947a59 /aarch64_small/armV8_common_lib.sail | |
| parent | 6aeb20251c94f391796d86d16deed70eee59d5ef (diff) | |
more
Diffstat (limited to 'aarch64_small/armV8_common_lib.sail')
| -rw-r--r-- | aarch64_small/armV8_common_lib.sail | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail index 5e8fc63c..aaf30c12 100644 --- a/aarch64_small/armV8_common_lib.sail +++ b/aarch64_small/armV8_common_lib.sail @@ -617,13 +617,14 @@ struct read_buffer_type = { size : uinteger, } -let empty_read_buffer = -{ size = 0; - /* arbitrary values: */ - acctype = AccType_NORMAL; - exclusive = false; - address = 0; -} +let empty_read_buffer : read_buffer_type = + struct { + size = 0, + /* arbitrary values: */ + acctype = AccType_NORMAL, + exclusive = false, + address = Zeros() + } val _rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, AddressDescriptor, atom('N), AccType, bool) -> read_buffer_type effect {escape} function _rMem(read_buffer, desc, size, acctype, exclusive) = { |