diff options
Diffstat (limited to 'mips/mips_prelude.sail')
| -rw-r--r-- | mips/mips_prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index b5931a45..7ec4fdfe 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -331,9 +331,9 @@ function wGPR (idx, v) = { if i == 0 then () else GPR[i] = v } -val MEMr = {lem: "MEMr"} : forall 'n. +val MEMr = {lem: "MEMr"} : forall 'n, 'n >= 0. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } -val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n. +val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n, 'n >= 0. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } val MEM_sync = {lem: "MEM_sync"} : unit -> unit effect { barr } |