diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/regfp.sail | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index 231ccf6e..86b3cf17 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -170,6 +170,11 @@ val __cache_maintenance : forall (constant 'addrsize : Int), 'addrsize in {32, 64}. (cache_op_kind, int('addrsize), bits('addrsize)) -> unit +val __instr_announce + = { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" } + : forall 'n, 'n > 0. + bits('n) -> unit + /* val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv} function __write (wk, addr, len, value) = { |