summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/c/config.expect6
-rw-r--r--test/c/config.sail34
-rwxr-xr-xtest/run_tests.sh14
-rw-r--r--test/sailtest.py2
-rw-r--r--test/typecheck/pass/commentfix.sail7
5 files changed, 56 insertions, 7 deletions
diff --git a/test/c/config.expect b/test/c/config.expect
new file mode 100644
index 00000000..059a413f
--- /dev/null
+++ b/test/c/config.expect
@@ -0,0 +1,6 @@
+x = 3
+Hello
+z = 0xFF
+x = 4
+World
+z = 0xAA
diff --git a/test/c/config.sail b/test/c/config.sail
new file mode 100644
index 00000000..2902d259
--- /dev/null
+++ b/test/c/config.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <arith.sail>
+$include <vector_dec.sail>
+
+val "print" : string -> unit
+
+register q : int
+
+register configuration x : int = 3
+
+register configuration y : string = "Hello\n"
+
+register configuration z : bits(8) = 0xFF
+
+val init : unit -> unit effect {configuration}
+
+function init() = {
+ x = 4;
+ y = "World\n";
+ z = 0xAA;
+}
+
+val main : unit -> unit effect {configuration}
+
+function main() = {
+ print_int("x = ", x);
+ print(y);
+ print_bits("z = ", z);
+ init();
+ print_int("x = ", x);
+ print(y);
+ print_bits("z = ", z);
+} \ No newline at end of file
diff --git a/test/run_tests.sh b/test/run_tests.sh
index 5e6fe691..ba0a2112 100755
--- a/test/run_tests.sh
+++ b/test/run_tests.sh
@@ -12,28 +12,28 @@ printf "==========================================\n"
./typecheck/run_tests.sh
printf "\n==========================================\n"
-printf "Ocaml tests\n"
+printf "Lem tests\n"
printf "==========================================\n"
-./ocaml/run_tests.sh
+./lem/run_tests.sh
printf "\n==========================================\n"
-printf "C tests\n"
+printf "Ocaml tests\n"
printf "==========================================\n"
-./c/run_tests.py
+./ocaml/run_tests.sh
printf "\n==========================================\n"
-printf "Lem tests\n"
+printf "C tests\n"
printf "==========================================\n"
-./lem/run_tests.sh
+TEST_PAR=8 ./c/run_tests.py
printf "\n==========================================\n"
printf "Builtins tests\n"
printf "==========================================\n"
-./builtins/run_tests.py
+TEST_PAR=4 ./builtins/run_tests.py
printf "\n==========================================\n"
printf "ARM spec tests\n"
diff --git a/test/sailtest.py b/test/sailtest.py
index 32d09aa9..5ee87b08 100644
--- a/test/sailtest.py
+++ b/test/sailtest.py
@@ -46,6 +46,7 @@ def banner(string):
print '-' * len(string)
print string
print '-' * len(string)
+ sys.stdout.flush()
class Results:
def __init__(self, name):
@@ -63,6 +64,7 @@ class Results:
else:
self.passes += 1
self.xml += ' <testcase name="{}"/>\n'.format(test)
+ sys.stdout.flush()
def finish(self):
print '{}{} passes and {} failures{}'.format(color.NOTICE, self.passes, self.failures, color.END)
diff --git a/test/typecheck/pass/commentfix.sail b/test/typecheck/pass/commentfix.sail
new file mode 100644
index 00000000..fd2cf0b2
--- /dev/null
+++ b/test/typecheck/pass/commentfix.sail
@@ -0,0 +1,7 @@
+/********/
+
+/*=====*/
+
+//////
+
+default Order inc