summaryrefslogtreecommitdiff
path: root/test/ocaml/hello_world
diff options
context:
space:
mode:
Diffstat (limited to 'test/ocaml/hello_world')
-rw-r--r--test/ocaml/hello_world/expect2
-rw-r--r--test/ocaml/hello_world/hello_world.sail19
2 files changed, 21 insertions, 0 deletions
diff --git a/test/ocaml/hello_world/expect b/test/ocaml/hello_world/expect
new file mode 100644
index 00000000..3df47a31
--- /dev/null
+++ b/test/ocaml/hello_world/expect
@@ -0,0 +1,2 @@
+Hello, Sail!
+Hello, World!
diff --git a/test/ocaml/hello_world/hello_world.sail b/test/ocaml/hello_world/hello_world.sail
new file mode 100644
index 00000000..d96429f2
--- /dev/null
+++ b/test/ocaml/hello_world/hello_world.sail
@@ -0,0 +1,19 @@
+
+val unit -> string effect pure hello_world
+
+function hello_world () = {
+ return "Hello, World!";
+ "Unreachable"
+}
+
+val unit -> unit effect {wreg, rreg} main
+
+register string REG
+
+function main () = {
+ REG := "Hello, Sail!";
+ print(REG);
+ REG := hello_world ();
+ print(REG);
+ return ()
+}