From f0b547154b3d2ce9e4bac74b0c56f20d6db76cd2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 17 May 2019 16:34:00 +0100 Subject: SMT: Finish adding all memory builtins from lib/regfp.sail --- lib/regfp.sail | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'lib') 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} -- cgit v1.2.3