test.vpr

import "foo.tdf"
import "foo.txt"
import "foo.txt"
domain Foo[T] {
 axiom named { forall x: Int:: {lookup(x)} len(lookup(x)) == foobar(x) }
 axiom { forall x: Int :: {lookup(x)} {len(lookup(x))} len(lookup(x)) == foobar(x) } // anonymous
}
// this is a comment
/* This is also
 * another multi-line comment
 * With a string "string" and
 * an import "foo.bar" inside */
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/
import "empty.sil"
method test1(xs: Seq[Ref]) {
 inhale forall i: Int :: 0 <= i && i < |xs| ==> xs[i].f != 0
}
function $(n: Ref, m: Ref): Node
domain Foo[T] {
 function enc(arg: T): Foo[T]
 function dec(arg: Foo[T]): T
 axiom ax_Dec {
 forall arg: T ::
 dec( enc(arg) ) == arg
 }
 axiom ax_Enc {
 forall arg: Foo[T] ::
 { enc( dec(arg) ), foo(bar, i) }
 { dec(arg) }
 enc( dec(arg) ) == arg
 }
}
function myFunc(arg: Int): Int
 requires true || false
 ensures arg <= 0 ==> result == -1
 ensures arg> 0 ==> result == arg
{
 arg> 0 ? arg : myFunc(arg - 1)
}
field value: Int
field next: Ref
predicate list(xs: Ref) {
 acc(xs.value) && acc(xs.next)
 && ( list(xs.next) )
}
define myPureMacro(abc) abc
define myStmtMacro(abc) {
 inhale abc
 exhale abc
}
method smokeTest() {
 inhale false; exhale false
 assume false; assert false
 //magic wands
 var s: Set[Int]
 assert s setminus s != s
}
//:: special comment
/*
 gfdgfd
*/
method testHighlights() returns ( res: Set[Seq[Multiset[Foo[Int]]]] )
 requires true
 ensures false
{
 var a: Int; var b: Bool; var c: Ref; var d: Rational; var e: Perm
 var x: Seq[Int]; var y: Set[Int]; var z: Multiset[Int]
 var t1: Set[Int] := Set(a, 1, 2)
 var t2: Seq[Int] := Seq(a, a, a)
 var t3: Multiset[Int] := Multiset(a, a, 0, 0, 0)
 assert myFunc(331)> -2
 myStmtMacro( myFunc(331) == -331 )
 while ( true )
 invariant true
 {
 var aa: Ref
 aa := null
 var bb: Int
 bb := 33
 }
 if ( true ) {
 assert true
 } elseif ( false ) {
 assert false
 } else {
 assert true
 }
 //forperm r: Ref :: true
 //exists
 //forall
 assert ! false
 assert 0 +321 - 0 -321 == 0
}
field f:Int
method test02(x: Ref)
 requires acc(x.f, write)
 ensures acc(x.f, write)
{
 define A true
 define B acc(x.f, write)
 package A --* B
 wand w := A --* B
 //apply w
 label my_lbl
 goto my_lbl
 fresh x
 var p: Perm
 var r: Ref; r := new (*)
 constraining ( p ) {
 exhale acc(x.f, p)
 }
 assert 0 == ( let a == (11 + 22) in a+a )
}