diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/ocaml/prelude.sail | 8 | ||||
| -rw-r--r-- | test/ocaml/reg_passing/reg_passing.sail | 3 | ||||
| -rwxr-xr-x | test/ocaml/run_tests.sh | 23 |
3 files changed, 31 insertions, 3 deletions
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index add43eec..6b8acb44 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -18,7 +18,10 @@ val eq_string = "eq_string" : (string, string) -> bool val eq_real = "eq_real" : (real, real) -> bool -val eq_anything = "(fun (x, y) -> x = y)" : forall ('a : Type). ('a, 'a) -> bool +val eq_anything = { + ocaml: "(fun (x, y) -> x = y)", + interpreter: "eq_anything" + } : forall ('a : Type). ('a, 'a) -> bool val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) @@ -141,6 +144,9 @@ val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) val cast cast_unit_vec : bit -> bits(1) +function cast_unit_vec bitone = 0b1 +and cast_unit_vec bitzero = 0b0 + val print = "print_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail index d84f98e0..35ddda93 100644 --- a/test/ocaml/reg_passing/reg_passing.sail +++ b/test/ocaml/reg_passing/reg_passing.sail @@ -5,7 +5,8 @@ register R3 : int val cast "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} val output = { - ocaml: "(fun (str, n) -> print_endline (str ^ string_of_big_int n))" + ocaml: "(fun (str, n) -> print_endline (str ^ string_of_big_int n))", + interpreter: "print_int" } : (string, int) -> unit val f : register(int) -> unit effect {rreg, wreg} diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index ccc3889e..62fe9950 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -81,7 +81,7 @@ do then green "built $i" "ok" else - yellow "bad output $i" "fail" + red "bad output $i" "fail" fi; rm out; rm result; @@ -93,4 +93,25 @@ done finish_suite "Ocaml trace testing" +cd $DIR + +for i in `ls -d */`; +do + cd $DIR/$i; + if $SAILDIR/sail -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null; + then + if diff expect result; + then + green "interpreted $i" "ok" + else + red "bad output $i" "fail" + fi; + rm result + else + red "interpreter crashed on $i" "fail" + fi +done + +finish_suite "Interpreter testing" + printf "</testsuites>\n" >> $DIR/tests.xml |