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

1 files changed, 2 insertions, 4 deletions

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;