aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_types.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_types.sail')
-rw-r--r--model/riscv_types.sail6
1 files changed, 3 insertions, 3 deletions
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 728c1d2..b940286 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -138,10 +138,10 @@ union exception = {
Error_internal_error : unit
}
-val not_implemented : forall ('a : Type). string -> 'a effect {escape}
+val not_implemented : forall ('a : Type). string -> 'a
function not_implemented message = throw(Error_not_implemented(message))
-val internal_error : forall ('a : Type). (string, int, string) -> 'a effect {escape}
+val internal_error : forall ('a : Type). (string, int, string) -> 'a
function internal_error(file, line, s) = {
assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s);
throw Error_internal_error()
@@ -464,7 +464,7 @@ function word_width_bytes width = match width {
* should be unreachable. See https://github.com/riscv/sail-riscv/issues/194
* and https://github.com/riscv/sail-riscv/pull/197 .
*/
-val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a effect {escape}
+val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a
function report_invalid_width(f , l, w, k) -> 'a = {
/*
* Ideally we would call internal_error here but this triggers a Sail bug,