Add some effects to execute function declarationand remove val specs for calling functions to allow effects to be inferred.

3 files changed, 4 insertions, 8 deletions

diff --git a/model/main.sail b/model/main.sail
index 8040bdb..9abe1a5 100644
--- a/model/main.sail
+++ b/model/main.sail
@@ -1,6 +1,4 @@
-val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
-
-function main () = {
+function main () : unit -> unit = {
   // initialize extensions
   ext_init ();
 
diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
index b007246..b27711b 100644
--- a/model/riscv_insts_begin.sail
+++ b/model/riscv_insts_begin.sail
@@ -6,7 +6,7 @@
 scattered union ast
 
 /* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem}
+val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, rmemt, barr, exmem, undef}
 scattered function execute
 
 val assembly : ast <-> string
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 2d3adf6..4e81fe9 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -1,8 +1,7 @@
 /* The emulator fetch-execute-interrupt dispatch loop. */
 
 /* returns whether to increment the step count in the trace */
-val step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wmvt, wreg}
-function step(step_no) = {
+function step(step_no : int) -> bool = {
   /* for step extensions */
   ext_pre_step_hook();
 
@@ -72,8 +71,7 @@ function step(step_no) = {
   stepped
 }
 
-val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wmvt, wreg}
-function loop () = {
+function loop () : unit -> unit = {
   let insns_per_tick = plat_insns_per_tick();
   i : int = 0;
   step_no : int = 0;