summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/value.ml1
-rwxr-xr-xtest/arm/run_tests.sh4
2 files changed, 3 insertions, 2 deletions
diff --git a/src/value.ml b/src/value.ml
index 41b52720..1d2346af 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -561,6 +561,7 @@ let primops =
("write_ram", value_write_ram);
("trace_memory_read", fun _ -> V_unit);
("trace_memory_write", fun _ -> V_unit);
+ ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns()));
("load_raw", value_load_raw);
("to_real", value_to_real);
("eq_real", value_eq_real);
diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh
index f758d634..30f955b0 100755
--- a/test/arm/run_tests.sh
+++ b/test/arm/run_tests.sh
@@ -51,7 +51,7 @@ cd $SAILDIR/aarch64
printf "Compiling specification...\n"
-if $SAILDIR/sail -no_lexp_bounds_check -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null;
+if $SAILDIR/sail -no_lexp_bounds_check -o aarch64_test -ocaml no_vector.sail 1> /dev/null 2> /dev/null;
then
green "compiled no_vector specification" "ok";
mv aarch64_test $DIR/;
@@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n"
cd $SAILDIR/aarch64
-if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null;
+if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail no_vector.sail 1> /dev/null 2> /dev/null;
then
green "loaded no_vector specification" "ok";