summaryrefslogtreecommitdiff
path: root/aarch64_small
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64_small')
-rw-r--r--aarch64_small/armV8_common_lib.sail12
1 files changed, 6 insertions, 6 deletions
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index aaf30c12..576da545 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -714,13 +714,13 @@ struct write_buffer_type = {
size : range(0,16),
}
-let empty_write_buffer = {
- size = 0;
+let empty_write_buffer : write_buffer_type = struct {
+ size = 0,
/* arbitrary values: */
- acctype = AccType_NORMAL;
- exclusive = false;
- address = 0;
- value = 0;
+ acctype = AccType_NORMAL,
+ exclusive = false,
+ address = Zeros(),
+ value = Zeros()
}
val _wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, AddressDescriptor, atom('N), AccType, bool, bits('N*8)) -> write_buffer_type effect {escape}