diff options
Diffstat (limited to 'Test/datatypes/t1.bpl')
-rw-r--r-- | Test/datatypes/t1.bpl | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl index f0488639..876d879d 100644 --- a/Test/datatypes/t1.bpl +++ b/Test/datatypes/t1.bpl @@ -1,26 +1,26 @@ -// RUN: %boogie -typeEncoding:m "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type TT;
-type {:datatype} Tree;
-function {:constructor} leaf() : Tree;
-function {:constructor} node(value:TT, children:TreeList) : Tree;
-
-type {:datatype} TreeList;
-function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;
-function {:constructor} nil() : TreeList;
-
-procedure foo()
-{
- var a: Tree;
- var b: TreeList;
- var x: TT;
-
- assert value#node(node(x, nil())) == x;
- assert children#node(node(x, nil())) == nil();
-
- assert (cons(leaf(), nil()) != nil());
-
- assert is#nil(nil());
-
- assert is#node(leaf());
+// RUN: %boogie -typeEncoding:m "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type TT; +type {:datatype} Tree; +function {:constructor} leaf() : Tree; +function {:constructor} node(value:TT, children:TreeList) : Tree; + +type {:datatype} TreeList; +function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList; +function {:constructor} nil() : TreeList; + +procedure foo() +{ + var a: Tree; + var b: TreeList; + var x: TT; + + assert value#node(node(x, nil())) == x; + assert children#node(node(x, nil())) == nil(); + + assert (cons(leaf(), nil()) != nil()); + + assert is#nil(nil()); + + assert is#node(leaf()); }
\ No newline at end of file |