diff options
| author | Alasdair Armstrong | 2018-07-30 19:16:34 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-08-01 16:42:33 +0100 |
| commit | 1479ae359fd3afebf9c3dfb6e58a77254e8140ea (patch) | |
| tree | ffcfd96409467a5c41009f68afe1f65a2c7a3d49 /src/test/test4.sail | |
| parent | 0b70a9d7464d6c30534d2f511cb8c9879c76b1e5 (diff) | |
Remove old test directory in src/test
Diffstat (limited to 'src/test/test4.sail')
| -rw-r--r-- | src/test/test4.sail | 67 |
1 files changed, 0 insertions, 67 deletions
diff --git a/src/test/test4.sail b/src/test/test4.sail deleted file mode 100644 index fa0133ca..00000000 --- a/src/test/test4.sail +++ /dev/null @@ -1,67 +0,0 @@ -(* hack to display log messages. Syntax: LOG(0) := "log message"; *) -val extern forall Type 'a . (nat, 'a) -> unit effect { wmem } LOG - -register (bit[1]) GPR0 -register (bit[1]) GPR1 - -let (vector <0, 2, inc, (register<bit[1] >)>) GPR = [ GPR0, GPR1 ] - -(* if we access GPR with a bit or a nat - doing the conversion in the - caller, works as expected *) -function unit good ((bit) RA ) = -{ - LOG(0) := "good"; - (nat) x := GPR[RA]; -} - -function unit good2 ((nat) RA ) = -{ - LOG(0) := "good2"; - (nat) x := GPR[RA]; -} - -(* but here, the first to_num_inc(RA) somehow inhibits the cast, - yielding to_num_inc(GPR0) instead of to_num_inc(0b0) *) -function unit bad ((bit[1]) RA ) = -{ - LOG(0) := "oldbad"; - (nat) x := GPR[RA]; -} - -(* and now, another bug - when DCR contains registers of bits instead of bit[0] *) - -register (bit) DCR0 -register (bit) DCR1 - -let (vector <0, 2, inc, (register<bit >)>) DCR = [ DCR0, DCR1 ] - -(* also fails only when passing RA as a vector, nat and bit work fine as - above; - error message is different though, and very disturbing: - "error: No matching patterns in case", corresponding to the DCR[RA] - expression *) -function unit bad2 ((bit[1]) RA ) = -{ - LOG(0) := "oldbad2"; - (nat) x := DCR[RA]; -} - - -function unit main () = { - LOG(0) := "init"; - - GPR[0] := 0b0; - GPR[1] := 0b1; - - DCR[0] := bitzero; - DCR[1] := bitone; - - good(bitzero); - good2(0); - - (* a first bug *) - bad(0b0); - - (* another bug :-) comment out first one to see it *) - bad2(0b0); -} |
