diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign1.sail | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CauseReg1.sail | 1 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CauseReg2.sail | 1 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CauseReg3.sail | 1 |
4 files changed, 7 insertions, 2 deletions
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index a3036e1f..68a6ee95 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,5 +1,7 @@ -val forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv -val forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv +val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv +val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv + +val cast forall Type 'a, Type 'b. 'a -> 'b effect pure cast_anything default Order dec diff --git a/test/typecheck/pass/mips_CauseReg1.sail b/test/typecheck/pass/mips_CauseReg1.sail index e05d0af8..b9503efa 100644 --- a/test/typecheck/pass/mips_CauseReg1.sail +++ b/test/typecheck/pass/mips_CauseReg1.sail @@ -1,3 +1,4 @@ +default Order dec typedef CauseReg = register bits [ 31 : 0 ] { 31 : BD; (* branch delay *) diff --git a/test/typecheck/pass/mips_CauseReg2.sail b/test/typecheck/pass/mips_CauseReg2.sail index f62824f1..7600c9f1 100644 --- a/test/typecheck/pass/mips_CauseReg2.sail +++ b/test/typecheck/pass/mips_CauseReg2.sail @@ -1,3 +1,4 @@ +default Order dec typedef CauseReg = register bits [ 31 : 1 ] { 31 : BD; (* branch delay *) diff --git a/test/typecheck/pass/mips_CauseReg3.sail b/test/typecheck/pass/mips_CauseReg3.sail index 24b07fcd..48acd4f5 100644 --- a/test/typecheck/pass/mips_CauseReg3.sail +++ b/test/typecheck/pass/mips_CauseReg3.sail @@ -1,3 +1,4 @@ +default Order dec typedef CauseReg = register bits [ 31 : 0 ] { 31 : BD; (* branch delay *) |