diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/bitwise_not_gen.sail | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/mips400.sail | 4 | ||||
| -rw-r--r-- | test/typecheck/pass/set_spsr.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/simple_scattered.sail | 2 |
4 files changed, 8 insertions, 6 deletions
diff --git a/test/typecheck/pass/bitwise_not_gen.sail b/test/typecheck/pass/bitwise_not_gen.sail index 8be3ea5c..6d36c566 100644 --- a/test/typecheck/pass/bitwise_not_gen.sail +++ b/test/typecheck/pass/bitwise_not_gen.sail @@ -2,7 +2,7 @@ val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not default Order dec - + val forall 'n. bit['n] -> bit['n] effect pure test - -function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file + +function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x)) diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail index 38680fcf..1e8691d9 100644 --- a/test/typecheck/pass/mips400.sail +++ b/test/typecheck/pass/mips400.sail @@ -13,7 +13,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec overload vector_subrange [vector_subrange_inc; vector_subrange_dec] @@ -491,7 +491,7 @@ register (bit[1]) UART_RVALID (* Check whether a given 64-bit vector is a properly sign extended 32-bit word *) val bit[64] -> bool effect pure NotWordVal -function bool NotWordVal (word) = +function bool NotWordVal (word) = (word[31] ^^ 32) != word[63..32] (* Read numbered GP reg. (r0 is always zero) *) diff --git a/test/typecheck/pass/set_spsr.sail b/test/typecheck/pass/set_spsr.sail index b30343a2..7fac206c 100644 --- a/test/typecheck/pass/set_spsr.sail +++ b/test/typecheck/pass/set_spsr.sail @@ -4,7 +4,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec overload vector_subrange [vector_subrange_inc; vector_subrange_dec] diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail index 41479888..a500cd1f 100644 --- a/test/typecheck/pass/simple_scattered.sail +++ b/test/typecheck/pass/simple_scattered.sail @@ -10,6 +10,8 @@ scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execu union ast member (bit[8], bit['regsize]) test +union ast member int test2 + function clause execute (test (x, y)) = { return () |