autotests/input/test.vpr

0001 import "foo.tdf"
0002 import "foo.txt"
0003 import "foo.txt"
0004
0005 domain Foo[T] {
0006     axiom named { forall x: Int:: {lookup(x)} len(lookup(x)) == foobar(x) }
0007     axiom { forall x: Int :: {lookup(x)} {len(lookup(x))} len(lookup(x)) == foobar(x) } // anonymous
0008 }
0009
0010 // this is a comment
0011
0012 /* This is also
0013  * another multi-line comment
0014  * With a string "string" and
0015  * an import "foo.bar" inside */
0016
0017 // Any copyright is dedicated to the Public Domain.
0018 // http://creativecommons.org/publicdomain/zero/1.0/
0019
0020 import "empty.sil"
0021
0022 method test1(xs: Seq[Ref]) {
0023   inhale forall i: Int :: 0 <= i && i < |xs| ==> xs[i].f != 0
0024 }
0025
0026 function $(n: Ref, m: Ref): Node
0027
0028 domain Foo[T] {
0029     function enc(arg: T): Foo[T]
0030     function dec(arg: Foo[T]): T
0031
0032     axiom ax_Dec {
0033         forall arg: T ::
0034             dec( enc(arg) ) == arg
0035     }
0036
0037     axiom ax_Enc {
0038         forall arg: Foo[T] ::
0039         { enc( dec(arg) ), foo(bar, i) }
0040             {  dec(arg) }
0041                 enc( dec(arg) ) == arg
0042     }
0043 }
0044
0045 function myFunc(arg: Int): Int
0046     requires true || false
0047     ensures arg <= 0 ==> result == -1
0048     ensures arg > 0  ==> result == arg
0049 {
0050     arg > 0 ? arg : myFunc(arg - 1)
0051 }
0052
0053 field value: Int
0054 field next: Ref
0055
0056 predicate list(xs: Ref) {
0057     acc(xs.value) && acc(xs.next)
0058     && ( list(xs.next) )
0059 }
0060
0061 define myPureMacro(abc) abc
0062
0063 define myStmtMacro(abc) {
0064     inhale abc
0065     exhale abc
0066 }
0067
0068 method smokeTest() {
0069
0070     inhale false; exhale false
0071     assume false; assert false
0072
0073     //magic wands
0074     var s: Set[Int]
0075     assert s setminus s != s
0076
0077 }
0078
0079 //:: special comment
0080 /*
0081         gfdgfd
0082 */
0083
0084 method testHighlights() returns ( res: Set[Seq[Multiset[Foo[Int]]]] )
0085     requires true
0086     ensures false
0087 {
0088     var a: Int; var b: Bool; var c: Ref; var d: Rational; var e: Perm
0089     var x: Seq[Int]; var y: Set[Int]; var z: Multiset[Int]
0090     var t1: Set[Int] := Set(a, 1, 2)
0091     var t2: Seq[Int] := Seq(a, a, a)
0092     var t3: Multiset[Int] := Multiset(a, a, 0, 0, 0)
0093
0094     assert myFunc(331) > -2
0095
0096     myStmtMacro( myFunc(331) == -331 )
0097
0098     while ( true )
0099         invariant true
0100     {
0101         var aa: Ref
0102         aa := null
0103         var bb: Int
0104         bb := 33
0105     }
0106
0107     if ( true ) {
0108         assert true
0109     } elseif ( false ) {
0110         assert false
0111     } else {
0112         assert true
0113     }
0114
0115     //forperm r: Ref :: true
0116     //exists
0117     //forall
0118     assert ! false
0119     assert 0  +321 - 0 -321 == 0
0120 }
0121
0122 field f:Int
0123
0124 method test02(x: Ref)
0125   requires acc(x.f, write)
0126   ensures acc(x.f, write)
0127 {
0128   define A true
0129   define B acc(x.f, write)
0130
0131   package A --* B
0132   wand w := A --* B
0133
0134   //apply w
0135
0136     label my_lbl
0137
0138     goto my_lbl
0139
0140     fresh x
0141
0142     var p: Perm
0143
0144     var r: Ref; r := new (*)
0145
0146     constraining ( p ) {
0147         exhale acc(x.f, p)
0148     }
0149
0150     assert 0 == ( let a == (11 + 22) in a+a )
0151 }