Add an __instr_announce builtin in regfp.sail

Allows keeping track of which instructions actually get executed in a trace

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) = {