summaryrefslogtreecommitdiff
path: root/Test/datatypes/t2.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/datatypes/t2.bpl')
-rw-r--r--Test/datatypes/t2.bpl50
1 files changed, 25 insertions, 25 deletions
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl
index 106b8d0c..257fff9c 100644
--- a/Test/datatypes/t2.bpl
+++ b/Test/datatypes/t2.bpl
@@ -1,26 +1,26 @@
-// RUN: %boogie -typeEncoding:m "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type TT;
-type {:datatype} Tree;
-function {:constructor} leaf`0() : Tree;
-function {:constructor} node`2(value:TT, children:TreeList) : Tree;
-
-type {:datatype} TreeList;
-function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;
-function {:constructor} nil`0() : TreeList;
-
-procedure foo()
-{
- var a: Tree;
- var b: TreeList;
- var x: TT;
-
- assert value#node`2(node`2(x, nil`0())) == x;
- assert children#node`2(node`2(x, nil`0())) == nil`0();
-
- assert (cons`2(leaf`0(), nil`0()) != nil`0());
-
- assert is#nil`0(nil`0());
-
- assert is#node`2(leaf`0());
+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type TT;
+type {:datatype} Tree;
+function {:constructor} leaf`0() : Tree;
+function {:constructor} node`2(value:TT, children:TreeList) : Tree;
+
+type {:datatype} TreeList;
+function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil`0() : TreeList;
+
+procedure foo()
+{
+ var a: Tree;
+ var b: TreeList;
+ var x: TT;
+
+ assert value#node`2(node`2(x, nil`0())) == x;
+ assert children#node`2(node`2(x, nil`0())) == nil`0();
+
+ assert (cons`2(leaf`0(), nil`0()) != nil`0());
+
+ assert is#nil`0(nil`0());
+
+ assert is#node`2(leaf`0());
} \ No newline at end of file