diff options
| author | Alasdair Armstrong | 2017-11-10 18:39:51 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-10 18:39:51 +0000 |
| commit | d7ee7d7392d7d4f058cce2e12b7d0336dddb4e17 (patch) | |
| tree | c953db8e1780a7b80e2f093b72e62047834278c7 /test | |
| parent | 05a84d17bf583c97fb3e77c4a6a07d888a6a2681 (diff) | |
Fixed ocaml backend so it correctly compiles registers passed by name.
Added a test case for this behavior
Diffstat (limited to 'test')
| -rw-r--r-- | test/ocaml/reg_passing/expect | 3 | ||||
| -rw-r--r-- | test/ocaml/reg_passing/reg_passing.sail | 36 |
2 files changed, 39 insertions, 0 deletions
diff --git a/test/ocaml/reg_passing/expect b/test/ocaml/reg_passing/expect new file mode 100644 index 00000000..e64f92f2 --- /dev/null +++ b/test/ocaml/reg_passing/expect @@ -0,0 +1,3 @@ +R1 = 10 +R2 = 20 +R3 = 10 diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail new file mode 100644 index 00000000..94acdf7e --- /dev/null +++ b/test/ocaml/reg_passing/reg_passing.sail @@ -0,0 +1,36 @@ + +register R1 : int +register R2 : int +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))" + } : (string, int) -> unit + +val f : register(int) -> unit effect {rreg, wreg} + +function f R = { + R1 = R; +} + +val g : unit -> unit effect {rreg, wreg} + +function g () = { + f(R1); + f(R2); +} + +val main : unit -> unit effect {rreg, wreg} + +function main () = { + R1 = 4; + R2 = 5; + g (); + R3 = 10; + f(R3); + R2 = 20; + output("R1 = ", R1); + output("R2 = ", R2); + output("R3 = ", R3) +}
\ No newline at end of file |
