summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/main.ml3
-rw-r--r--src/sail_lib.ml8
2 files changed, 10 insertions, 1 deletions
diff --git a/lib/main.ml b/lib/main.ml
index c1b6fcae..a3541c69 100644
--- a/lib/main.ml
+++ b/lib/main.ml
@@ -60,7 +60,8 @@ let options = Arg.align [
| [fname;addr] -> (fname, Nat_big_num.of_string addr)
| _ -> raise (Arg.Bad (s ^ " not of form <filename>@<addr>")) in
opt_raw_files := (file, addr) :: !opt_raw_files),
- "<file@0xADDR> load a raw binary in memory at given address.")]
+ "<file@0xADDR> load a raw binary in memory at given address.");
+ ("-cycle-limit", Arg.Set_int (Sail_lib.opt_cycle_limit), "<int> exit after given number of instructions executed.")]
let usage_msg = "Sail OCaml RTS options:"
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 8251f9b4..03994657 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -17,6 +17,14 @@ let opt_trace = ref false
let trace_depth = ref 0
let random = ref false
+
+let opt_cycle_limit = ref 0
+let cycle_count = ref 0
+
+let cycle_limit_reached () =
+ cycle_count := !cycle_count + 1;
+ !opt_cycle_limit != 0 && !cycle_count >= !opt_cycle_limit
+
let sail_call (type t) (f : _ -> t) =
let module M =
struct exception Return of t end