summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-05-17 16:34:00 +0100
committerAlasdair Armstrong2019-05-17 16:34:00 +0100
commitf0b547154b3d2ce9e4bac74b0c56f20d6db76cd2 (patch)
treeb6d1053bea33a115879fe24b4c5e6add0bae566e /lib
parent4a95bb1c25fe84be62f6eada024f964472736e69 (diff)
SMT: Finish adding all memory builtins from lib/regfp.sail
Diffstat (limited to 'lib')
-rw-r--r--lib/regfp.sail6
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail
index ebbf1655..da9c11d6 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -120,10 +120,12 @@ val __read_mem
(read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem}
val __write_mem_ea
= { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
- : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem}
+ : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
+ (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem}
val __write_mem
= { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
- : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
+ : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
+ (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
val __excl_res
= { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
: unit -> bool effect {exmem}