summaryrefslogtreecommitdiff
path: root/Test/test20/TypeDecls0.bpl
diff options
context:
space:
mode:
authorGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
committerGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
commitce1c2de044c91624370411e23acab13b0381949b (patch)
tree592539996fe08050ead5ee210c973801611dde40 /Test/test20/TypeDecls0.bpl
Initial set of files.
Diffstat (limited to 'Test/test20/TypeDecls0.bpl')
-rw-r--r--Test/test20/TypeDecls0.bpl45
1 files changed, 45 insertions, 0 deletions
diff --git a/Test/test20/TypeDecls0.bpl b/Test/test20/TypeDecls0.bpl
new file mode 100644
index 00000000..898e0d1a
--- /dev/null
+++ b/Test/test20/TypeDecls0.bpl
@@ -0,0 +1,45 @@
+type C a _ b;
+type D;
+type E _;
+
+var A0 : D;
+
+var A1 : C D D D;
+
+var A2 : <a,b> [b, C a b D] C a D [D]a;
+
+var A3 : <a,b> [b, C a int D] C bool ref [bv32]a;
+
+var A4 : <a,a> [a] a; // error: a bound twice
+var A5 : <a> [a] <a> [a] int; // error: a bound twice
+
+var A6 : <a> [a] <b> [b] int;
+
+var A7 : <a> [a] <b> [int] int; // error: b does not occur as map argument
+
+type C _ _; // error: C is already declared
+
+var A8 : C int ref; // error: wrong number of arguments
+
+var A9 : A0; // error: undeclared type
+var A10: F int; // error: undeclared type
+
+var A11: E D;
+var A12: E E D; // error: wrong number of arguments
+var A13: E (E D);
+var A14: E E E D; // error: wrong number of arguments
+
+var A15: E E int; // error: wrong number of arguments
+var A16: E (E int);
+
+var A17: bv64;
+var A18: [int] bv64;
+
+var A19: C E E D; // error: wrong number of arguments
+var A20: C (E (E D)) int [int] int;
+var A21: C (<a> [a] <b> [b] int) int [int] int;
+
+var A22: (D);
+var A23: ((D));
+
+type ref;