From 2dcb445f1addae38aff40d5a153952ee7b4130e5 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 5 Jun 2014 14:57:27 +0200 Subject: Made the snapshotable trees test "unsupported" instead of "unresolved". --- Test/dafny2/SnapshotableTrees.dfy | 480 -------------------------- Test/dafny2/unsupported/SnapshotableTrees.dfy | 480 ++++++++++++++++++++++++++ Test/dafny2/unsupported/lit.local.cfg | 2 + 3 files changed, 482 insertions(+), 480 deletions(-) delete mode 100644 Test/dafny2/SnapshotableTrees.dfy create mode 100644 Test/dafny2/unsupported/SnapshotableTrees.dfy create mode 100644 Test/dafny2/unsupported/lit.local.cfg (limited to 'Test/dafny2') diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy deleted file mode 100644 index 2c7a91df..00000000 --- a/Test/dafny2/SnapshotableTrees.dfy +++ /dev/null @@ -1,480 +0,0 @@ -// Rustan Leino, September 2011. -// This file contains a version of the C5 library's snapshotable trees. A different verification -// of a version like this has been done by Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and -// Peter Sestoft in separation logic using Coq. - -method Main() -{ - var t := new Tree.Empty(); - ghost var pos := t.Insert(2); - pos := t.Insert(1); - pos := t.Insert(3); - pos := t.Insert(-15); - pos := t.Insert(0); - - var s := t.CreateSnapshot(); - ghost var sc := s.Contents; - var it := s.CreateIterator(); - var more := it.MoveNext(); - while (more) - invariant t.Valid() && !t.IsReadonly && it.Valid(); - invariant more ==> 0 <= it.N < |it.Contents|; - invariant fresh(t.Repr) && fresh(it.IterRepr) && t.MutableRepr !! it.T.Repr && t.Repr !! it.IterRepr; - invariant it.T == s && s.Valid() && s.Contents == sc; // this is not needed in the loop, but serves as an extra test case of the specifications - decreases |it.Contents| - it.N; - { - var x := it.Current(); - print "Main iterates on ", x, "\n"; - pos := t.Insert(x*3); - more := it.MoveNext(); - } - assert s.Contents == sc; // this is not needed in the loop, but serves as an extra test case of the specifications - t.Print(); -} - -method TestContents() // this method tests Tree.Insert's specifications of Contents -{ - var t := new Tree.Empty(); assert t.Contents == []; - ghost var pos := t.Insert(2); assert pos == 0 && t.Contents == [2]; - - pos := t.Insert(1); - // Convince the verifier of the absurdity of pos==1 - assert pos == 1 ==> t.Contents == [2,1]; - ghost var hc := [2,1]; - assert hc[0] == 2 && hc[1] == 1 && !Tree.IsSorted(hc); - // So: - assert pos == 0 && t.Contents == [1, 2]; -} - -class Tree -{ - // public - ghost var Contents: seq; - var IsReadonly: bool; - ghost var Repr: set; - ghost var MutableRepr: set; - // private - var root: Node; - var reprIsShared: bool; - - function Valid(): bool - reads this, Repr; - { - this in MutableRepr && MutableRepr <= Repr && null !in Repr && - (root == null ==> Contents == []) && - (root != null ==> - root in Repr && root.Repr <= Repr && this !in root.Repr && - root.Valid() && Contents == root.Contents) && - IsSorted(Contents) && - (IsReadonly ==> reprIsShared) && - (!reprIsShared && root != null ==> root.Repr <= MutableRepr) && - (reprIsShared ==> MutableRepr == {this}) - } - - static function IsSorted(c: seq): bool // checks if "c" is sorted and has no duplicates - { - forall i, j :: 0 <= i < j < |c| ==> c[i] < c[j] - } - - constructor Empty() - modifies this; - ensures Valid() && Contents == [] && !IsReadonly; - ensures fresh(Repr - {this}); - { - Contents := []; - IsReadonly := false; - MutableRepr := {this}; - Repr := MutableRepr; - root := null; - reprIsShared := false; - } - - method CreateSnapshot() returns (snapshot: Tree) - requires Valid(); - modifies Repr; - ensures Valid() && fresh(Repr - old(Repr)); - ensures Contents == old(Contents) && IsReadonly == old(IsReadonly); - ensures snapshot != null && snapshot.Valid(); - ensures snapshot.Contents == Contents && snapshot.IsReadonly; - // the mutable part of the original tree is disjoint from the representation of the snapshot - ensures snapshot.Repr !! MutableRepr; - // representation of the snapshot consists of new things of things from the previous tree (that are now immutable) - ensures fresh(snapshot.Repr - old(Repr)); - { - // from now on, only "this" is mutable; the rest of the representation is immutable - Repr := Repr + MutableRepr; - MutableRepr := {this}; - reprIsShared := true; - snapshot := new Tree.Private(); - snapshot.Contents := Contents; - snapshot.IsReadonly := true; - snapshot.MutableRepr := {snapshot}; - snapshot.Repr := Repr - {this} + {snapshot}; - snapshot.root := root; - snapshot.reprIsShared := true; - } - - // private - constructor Private() { } - - method Insert(x: int) returns (ghost pos: int) - requires Valid() && !IsReadonly; - modifies MutableRepr; - ensures Valid() && fresh(Repr - old(Repr)) && fresh(MutableRepr - old(MutableRepr)); - ensures IsReadonly == old(IsReadonly); - ensures x in old(Contents) ==> pos < 0 && Contents == old(Contents); - ensures x !in old(Contents) ==> - 0 <= pos < |Contents| == |old(Contents)| + 1 && - Contents == old(Contents[..pos] + [x] + Contents[pos..]); - { - if (reprIsShared) { - root, pos := Node.FunctionalInsert(root, x); - Contents := root.Contents; - Repr := root.Repr + {this}; - MutableRepr := {this}; - } else if (root == null) { - root := new Node.Init(x); - Contents := root.Contents; - pos := 0; - MutableRepr := root.Repr + {this}; - Repr := MutableRepr; - } else { - pos := root.MutatingInsert(x); - Contents := root.Contents; - MutableRepr := MutableRepr + root.Repr; - Repr := MutableRepr; - } - } - - method CreateIterator() returns (iter: Iterator) - requires Valid(); // && IsReadonly; - ensures iter != null && iter.Valid() && fresh(iter.IterRepr); - ensures iter.T == this && iter.Contents == Contents && iter.N == -1; - { - iter := new Iterator.Init(this); - } - - method Print() - requires Valid(); - modifies Repr; - ensures Valid() && fresh(Repr - old(Repr)); - ensures Contents == old(Contents) && IsReadonly == old(IsReadonly); - { - print "Tree:"; - var s := CreateSnapshot(); - var it := s.CreateIterator(); - var more := it.MoveNext(); - while (more) - invariant Valid() && fresh(Repr - old(Repr)) && Contents == old(Contents) && IsReadonly == old(IsReadonly); - invariant it.Valid(); - invariant more ==> 0 <= it.N < |it.Contents|; - invariant fresh(it.IterRepr) && MutableRepr !! it.T.Repr && Repr !! it.IterRepr; - decreases |it.Contents| - it.N; - { - var x := it.Current(); - print " ", x; - more := it.MoveNext(); - } - print "\n"; - } -} - -class Node -{ - ghost var Contents: seq; - ghost var Repr: set; - var data: int; - var left: Node; - var right: Node; - - function Valid(): bool - reads this, Repr; - { - this in Repr && null !in Repr && - (left != null ==> - left in Repr && left.Repr <= Repr && this !in left.Repr && left.Valid()) && - (right != null ==> - right in Repr && right.Repr <= Repr && this !in right.Repr && right.Valid()) && - (left == null && right == null ==> Contents == [data]) && - (left != null && right == null ==> Contents == left.Contents + [data]) && - (left == null && right != null ==> Contents == [data] + right.Contents) && - (left != null && right != null ==> Contents == left.Contents + [data] + right.Contents && left.Repr !! right.Repr) && - Tree.IsSorted(Contents) - } - - constructor Init(x: int) - modifies this; - ensures Valid() && fresh(Repr - {this}); - ensures Contents == [x]; - { - Contents := [x]; - Repr := {this}; - left, data, right := null, x, null; - } - - constructor Build(left: Node, x: int, right: Node) - requires this != left && this != right; - requires left != null ==> left.Valid() && this !in left.Repr && - forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < x; - requires right != null ==> right.Valid() && this !in right.Repr && - forall i :: 0 <= i < |right.Contents| ==> x < right.Contents[i]; - requires left != null && right != null ==> left.Repr !! right.Repr; - modifies this; - ensures Valid(); - ensures left == null && right == null ==> Contents == [x] && fresh(Repr - {this}); - ensures left != null && right == null ==> Contents == left.Contents + [x] && fresh(Repr - {this} - left.Repr); - ensures left == null && right != null ==> Contents == [x] + right.Contents && fresh(Repr - {this} - right.Repr); - ensures left != null && right != null ==> Contents == left.Contents + [x] + right.Contents && fresh(Repr - {this} - left.Repr - right.Repr); - { - Contents := [x]; - Repr := {this}; - this.left, data, this.right := left, x, right; - if (left != null) { - Contents := left.Contents + Contents; - Repr := Repr + left.Repr; - } - if (right != null) { - Contents := Contents + right.Contents; - Repr := Repr + right.Repr; - } - } - - static method FunctionalInsert(n: Node, x: int) returns (r: Node, ghost pos: int) - requires n != null ==> n.Valid(); - ensures r != null && r.Valid(); - ensures n == null ==> fresh(r.Repr); - ensures n != null ==> fresh(r.Repr - n.Repr); - ensures n == null ==> r.Contents == [x] && pos == 0; - ensures n != null && x in n.Contents ==> r == n && pos < 0; - ensures n != null && x !in n.Contents ==> - 0 <= pos < |r.Contents| == |n.Contents| + 1 && - r.Contents == n.Contents[..pos] + [x] + n.Contents[pos..]; - decreases if n == null then {} else n.Repr; - { - if (n == null) { - r := new Node.Init(x); - pos := 0; - } else if (x < n.data) { - var left; - assert n.left != null ==> n.data == n.Contents[|n.left.Contents|]; - assert n.left == null ==> n.data == n.Contents[0]; - left, pos := FunctionalInsert(n.left, x); - assert n.left == old(n.left); - if (left == n.left) { - r, pos := n, -1; - } else { - assert n.left != null ==> forall i :: 0 <= i < |n.left.Contents| ==> n.Contents[i] < n.data; - assert forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < n.data; - r := new Node.Build(left, n.data, n.right); - } - } else if (n.data < x) { - var right; - assert n.left != null ==> n.data == n.Contents[|n.left.Contents|]; - assert n.left == null ==> n.data == n.Contents[0]; - right, pos := FunctionalInsert(n.right, x); - if (right == n.right) { - assert n != null && x in n.Contents; - r, pos := n, -1; - } else { - assert n.left != null ==> forall i :: 0 <= i < |n.left.Contents| ==> n.left.Contents[i] < n.data; - assert forall i :: 0 <= i < |right.Contents| ==> n.data < right.Contents[i]; - r := new Node.Build(n.left, n.data, right); - pos := pos + 1 + if n.left == null then 0 else |n.left.Contents|; - assert n != null && x !in n.Contents ==> r.Contents == n.Contents[..pos] + [x] + n.Contents[pos..]; - } - } else { - r, pos := n, -1; - } - } - - method MutatingInsert(x: int) returns (ghost pos: int) - requires Valid(); - modifies Repr; - ensures Valid() && fresh(Repr - old(Repr)); - ensures x in old(Contents) ==> pos < 0 && Contents == old(Contents); - ensures x !in old(Contents) ==> - 0 <= pos < |Contents| == |old(Contents)| + 1 && - Contents == old(Contents[..pos] + [x] + Contents[pos..]); - decreases Repr; - { - assert data == Contents[if left==null then 0 else |left.Contents|]; - if (x < data) { - assert right == null || x !in right.Contents; - assert right != null ==> forall i :: 0 <= i < |right.Contents| ==> x < right.Contents[i]; - if (left == null) { - left := new Node.Init(x); - pos := 0; - } else { - assert forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < data; - pos := left.MutatingInsert(x); - assert Tree.IsSorted(left.Contents); - assert right != null ==> Tree.IsSorted(right.Contents); - assert forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < data; - } - Repr := Repr + left.Repr; - Contents := left.Contents + [data] + if right == null then [] else right.Contents; - assert Tree.IsSorted(Contents); - } else if (data < x) { - assert left == null || x !in left.Contents; - assert left != null ==> forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < x; - if (right == null) { - right := new Node.Init(x); - pos := 1 + if left == null then 0 else |left.Contents|; - } else { - assert forall i :: 0 <= i < |right.Contents| ==> data < right.Contents[i]; - pos := right.MutatingInsert(x); - assert Tree.IsSorted(right.Contents); - assert left != null ==> Tree.IsSorted(left.Contents); - assert forall i :: 0 <= i < |right.Contents| ==> data < right.Contents[i]; - if (0 <= pos) { - pos := pos + 1 + if left == null then 0 else |left.Contents|; - assert (if left == null then [] else left.Contents) + [data] + right.Contents == old(Contents[..pos] + [x] + Contents[pos..]); - } - } - Repr := Repr + right.Repr; - Contents := (if left == null then [] else left.Contents) + [data] + right.Contents; - assert Tree.IsSorted(Contents); - } else { - pos := -1; - } - } -} - -class Iterator -{ - // public - ghost var IterRepr: set; // note, IterRepr does not include T.Repr - ghost var Contents: seq; - ghost var N: int; - var T: Tree; - // private - var initialized: bool; - var stack: List; - - function Valid(): bool - reads this, IterRepr, T, T.Repr; - { - this in IterRepr && null !in IterRepr && - T != null && T.Valid() && IterRepr !! T.Repr && - Contents == T.Contents && -1 <= N <= |Contents| && - (initialized <==> 0 <= N) && - (N < 0 ==> R(stack, 0, Contents, T.Repr)) && - (0 <= N ==> R(stack, N, Contents, T.Repr)) - } - - // R(wlist, n, C, Nodes) says that C[n..] are data items yet to be processed. - // In more detail, wlist is a stack of tree fragments, where the concatenation of the - // "load" of each tree fragment (from the top of the stack downwards) equals - // C[n..]. A tree fragment is either - // * for Nil, the empty fragment - // * for Cons(p, rest), fragment [p.data]+p.right.Contents - // In each case, R(wlist,n,C,Nodes) implies that the fragment wlist proper is a prefix of C[n..]. - // Nodes is (an overapproximation of) the set of nodes read by R. - static function R(wlist: List, n: int, C: seq, Nodes: set): bool - reads Nodes; - decreases wlist; - { - match wlist - case Nil => n == |C| - case Cons(p, rest) => - p != null && p in Nodes && p.Repr <= Nodes && p.Valid() && - 0 <= n < |C| && p.data == C[n] && - R(rest, n + 1 + if p.right==null then 0 else |p.right.Contents|, C, Nodes) && - p.Contents[if p.left==null then 0 else |p.left.Contents| ..] <= C[n..] - } - - constructor Init(t: Tree) - requires t != null && t.Valid() && this !in t.Repr; - modifies this; - ensures Valid() && fresh(IterRepr - {this}); - ensures T == t && Contents == t.Contents && N == -1; - { - T := t; - IterRepr := {this}; - Contents := T.Contents; - initialized, stack, N := false, Nil, -1; - if (t.root != null) { - stack := Push(stack, 0, t.root, Contents, T.Repr); - } - } - - // private - static method Push(stIn: List, ghost n: int, p: Node, ghost C: seq, ghost Nodes: set) returns (st: List) - requires p != null && p in Nodes && p.Repr <= Nodes && p.Valid(); - requires 0 <= n <= |C|; - requires p.Contents <= C[n..]; - requires R(stIn, n + |p.Contents|, C, Nodes); - ensures R(st, n, C, Nodes); - decreases p.Contents; - { - st := Cons(p, stIn); - - assert p.data == p.Contents[if p.left == null then 0 else |p.left.Contents|]; // lemma - if (p.left != null) { - st := Push(st, n, p.left, C, Nodes); - } - } - - method Current() returns (x: int) - requires Valid() && 0 <= N < |Contents|; - ensures x == Contents[N]; - { - match (stack) { - case Cons(y, rest) => x := y.data; - } - } - - method MoveNext() returns (hasCurrent: bool) - requires Valid() && N <= |Contents|; - modifies IterRepr; - ensures Valid() && fresh(IterRepr - old(IterRepr)) && T.Repr == old(T.Repr); - ensures Contents == old(Contents) && T == old(T); - ensures old(N) < |Contents| ==> N == old(N) + 1; - ensures old(N) == |Contents| ==> N == old(N); - ensures hasCurrent <==> 0 <= N < |Contents|; - { - if (!initialized) { - initialized, N := true, 0; - hasCurrent := stack != Nil; - } else { - match (stack) { - case Nil => - hasCurrent := false; - case Cons(p, rest) => - // lemmas: - assert R(rest, N + 1 + if p.right==null then 0 else |p.right.Contents|, Contents, T.Repr); - ghost var k := if p.left==null then 0 else |p.left.Contents|; - assert p.Contents[k..] == [p.data] + p.Contents[k+1..]; - assert p.Contents[k+1..] <= Contents[N+1..]; - - stack, N := rest, N+1; - - if (p.right != null) { - stack := Push(stack, N, p.right, Contents, T.Repr); - } - hasCurrent := stack != Nil; - } - } - match (stack) { case Nil => assert N == |Contents|; case Cons(p, rest) => assert N < |Contents|; } // lemma - } -} - -datatype List = Nil | Cons(Node, List); - -/* The following method shows the problem of concurrent modifications and shows that the - * design of the snapshotable trees herein handle this correctly. That is, after inserting - * into a tree that is being iterated, use of the associated iterator can no longer be - * proved to be correct. - * -method TestConcurrentModification(t: Tree) - requires t != null && t.Valid() && !t.IsReadonly; - modifies t.MutableRepr; -{ - var it := t.CreateIterator(); - var more := it.MoveNext(); - if (more) { - var pos := t.Insert(52); // this modification of the collection renders all associated iterators invalid - more := it.MoveNext(); // error: operation t.Insert may have made this iterator invalid - } -} -*/ diff --git a/Test/dafny2/unsupported/SnapshotableTrees.dfy b/Test/dafny2/unsupported/SnapshotableTrees.dfy new file mode 100644 index 00000000..2c7a91df --- /dev/null +++ b/Test/dafny2/unsupported/SnapshotableTrees.dfy @@ -0,0 +1,480 @@ +// Rustan Leino, September 2011. +// This file contains a version of the C5 library's snapshotable trees. A different verification +// of a version like this has been done by Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and +// Peter Sestoft in separation logic using Coq. + +method Main() +{ + var t := new Tree.Empty(); + ghost var pos := t.Insert(2); + pos := t.Insert(1); + pos := t.Insert(3); + pos := t.Insert(-15); + pos := t.Insert(0); + + var s := t.CreateSnapshot(); + ghost var sc := s.Contents; + var it := s.CreateIterator(); + var more := it.MoveNext(); + while (more) + invariant t.Valid() && !t.IsReadonly && it.Valid(); + invariant more ==> 0 <= it.N < |it.Contents|; + invariant fresh(t.Repr) && fresh(it.IterRepr) && t.MutableRepr !! it.T.Repr && t.Repr !! it.IterRepr; + invariant it.T == s && s.Valid() && s.Contents == sc; // this is not needed in the loop, but serves as an extra test case of the specifications + decreases |it.Contents| - it.N; + { + var x := it.Current(); + print "Main iterates on ", x, "\n"; + pos := t.Insert(x*3); + more := it.MoveNext(); + } + assert s.Contents == sc; // this is not needed in the loop, but serves as an extra test case of the specifications + t.Print(); +} + +method TestContents() // this method tests Tree.Insert's specifications of Contents +{ + var t := new Tree.Empty(); assert t.Contents == []; + ghost var pos := t.Insert(2); assert pos == 0 && t.Contents == [2]; + + pos := t.Insert(1); + // Convince the verifier of the absurdity of pos==1 + assert pos == 1 ==> t.Contents == [2,1]; + ghost var hc := [2,1]; + assert hc[0] == 2 && hc[1] == 1 && !Tree.IsSorted(hc); + // So: + assert pos == 0 && t.Contents == [1, 2]; +} + +class Tree +{ + // public + ghost var Contents: seq; + var IsReadonly: bool; + ghost var Repr: set; + ghost var MutableRepr: set; + // private + var root: Node; + var reprIsShared: bool; + + function Valid(): bool + reads this, Repr; + { + this in MutableRepr && MutableRepr <= Repr && null !in Repr && + (root == null ==> Contents == []) && + (root != null ==> + root in Repr && root.Repr <= Repr && this !in root.Repr && + root.Valid() && Contents == root.Contents) && + IsSorted(Contents) && + (IsReadonly ==> reprIsShared) && + (!reprIsShared && root != null ==> root.Repr <= MutableRepr) && + (reprIsShared ==> MutableRepr == {this}) + } + + static function IsSorted(c: seq): bool // checks if "c" is sorted and has no duplicates + { + forall i, j :: 0 <= i < j < |c| ==> c[i] < c[j] + } + + constructor Empty() + modifies this; + ensures Valid() && Contents == [] && !IsReadonly; + ensures fresh(Repr - {this}); + { + Contents := []; + IsReadonly := false; + MutableRepr := {this}; + Repr := MutableRepr; + root := null; + reprIsShared := false; + } + + method CreateSnapshot() returns (snapshot: Tree) + requires Valid(); + modifies Repr; + ensures Valid() && fresh(Repr - old(Repr)); + ensures Contents == old(Contents) && IsReadonly == old(IsReadonly); + ensures snapshot != null && snapshot.Valid(); + ensures snapshot.Contents == Contents && snapshot.IsReadonly; + // the mutable part of the original tree is disjoint from the representation of the snapshot + ensures snapshot.Repr !! MutableRepr; + // representation of the snapshot consists of new things of things from the previous tree (that are now immutable) + ensures fresh(snapshot.Repr - old(Repr)); + { + // from now on, only "this" is mutable; the rest of the representation is immutable + Repr := Repr + MutableRepr; + MutableRepr := {this}; + reprIsShared := true; + snapshot := new Tree.Private(); + snapshot.Contents := Contents; + snapshot.IsReadonly := true; + snapshot.MutableRepr := {snapshot}; + snapshot.Repr := Repr - {this} + {snapshot}; + snapshot.root := root; + snapshot.reprIsShared := true; + } + + // private + constructor Private() { } + + method Insert(x: int) returns (ghost pos: int) + requires Valid() && !IsReadonly; + modifies MutableRepr; + ensures Valid() && fresh(Repr - old(Repr)) && fresh(MutableRepr - old(MutableRepr)); + ensures IsReadonly == old(IsReadonly); + ensures x in old(Contents) ==> pos < 0 && Contents == old(Contents); + ensures x !in old(Contents) ==> + 0 <= pos < |Contents| == |old(Contents)| + 1 && + Contents == old(Contents[..pos] + [x] + Contents[pos..]); + { + if (reprIsShared) { + root, pos := Node.FunctionalInsert(root, x); + Contents := root.Contents; + Repr := root.Repr + {this}; + MutableRepr := {this}; + } else if (root == null) { + root := new Node.Init(x); + Contents := root.Contents; + pos := 0; + MutableRepr := root.Repr + {this}; + Repr := MutableRepr; + } else { + pos := root.MutatingInsert(x); + Contents := root.Contents; + MutableRepr := MutableRepr + root.Repr; + Repr := MutableRepr; + } + } + + method CreateIterator() returns (iter: Iterator) + requires Valid(); // && IsReadonly; + ensures iter != null && iter.Valid() && fresh(iter.IterRepr); + ensures iter.T == this && iter.Contents == Contents && iter.N == -1; + { + iter := new Iterator.Init(this); + } + + method Print() + requires Valid(); + modifies Repr; + ensures Valid() && fresh(Repr - old(Repr)); + ensures Contents == old(Contents) && IsReadonly == old(IsReadonly); + { + print "Tree:"; + var s := CreateSnapshot(); + var it := s.CreateIterator(); + var more := it.MoveNext(); + while (more) + invariant Valid() && fresh(Repr - old(Repr)) && Contents == old(Contents) && IsReadonly == old(IsReadonly); + invariant it.Valid(); + invariant more ==> 0 <= it.N < |it.Contents|; + invariant fresh(it.IterRepr) && MutableRepr !! it.T.Repr && Repr !! it.IterRepr; + decreases |it.Contents| - it.N; + { + var x := it.Current(); + print " ", x; + more := it.MoveNext(); + } + print "\n"; + } +} + +class Node +{ + ghost var Contents: seq; + ghost var Repr: set; + var data: int; + var left: Node; + var right: Node; + + function Valid(): bool + reads this, Repr; + { + this in Repr && null !in Repr && + (left != null ==> + left in Repr && left.Repr <= Repr && this !in left.Repr && left.Valid()) && + (right != null ==> + right in Repr && right.Repr <= Repr && this !in right.Repr && right.Valid()) && + (left == null && right == null ==> Contents == [data]) && + (left != null && right == null ==> Contents == left.Contents + [data]) && + (left == null && right != null ==> Contents == [data] + right.Contents) && + (left != null && right != null ==> Contents == left.Contents + [data] + right.Contents && left.Repr !! right.Repr) && + Tree.IsSorted(Contents) + } + + constructor Init(x: int) + modifies this; + ensures Valid() && fresh(Repr - {this}); + ensures Contents == [x]; + { + Contents := [x]; + Repr := {this}; + left, data, right := null, x, null; + } + + constructor Build(left: Node, x: int, right: Node) + requires this != left && this != right; + requires left != null ==> left.Valid() && this !in left.Repr && + forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < x; + requires right != null ==> right.Valid() && this !in right.Repr && + forall i :: 0 <= i < |right.Contents| ==> x < right.Contents[i]; + requires left != null && right != null ==> left.Repr !! right.Repr; + modifies this; + ensures Valid(); + ensures left == null && right == null ==> Contents == [x] && fresh(Repr - {this}); + ensures left != null && right == null ==> Contents == left.Contents + [x] && fresh(Repr - {this} - left.Repr); + ensures left == null && right != null ==> Contents == [x] + right.Contents && fresh(Repr - {this} - right.Repr); + ensures left != null && right != null ==> Contents == left.Contents + [x] + right.Contents && fresh(Repr - {this} - left.Repr - right.Repr); + { + Contents := [x]; + Repr := {this}; + this.left, data, this.right := left, x, right; + if (left != null) { + Contents := left.Contents + Contents; + Repr := Repr + left.Repr; + } + if (right != null) { + Contents := Contents + right.Contents; + Repr := Repr + right.Repr; + } + } + + static method FunctionalInsert(n: Node, x: int) returns (r: Node, ghost pos: int) + requires n != null ==> n.Valid(); + ensures r != null && r.Valid(); + ensures n == null ==> fresh(r.Repr); + ensures n != null ==> fresh(r.Repr - n.Repr); + ensures n == null ==> r.Contents == [x] && pos == 0; + ensures n != null && x in n.Contents ==> r == n && pos < 0; + ensures n != null && x !in n.Contents ==> + 0 <= pos < |r.Contents| == |n.Contents| + 1 && + r.Contents == n.Contents[..pos] + [x] + n.Contents[pos..]; + decreases if n == null then {} else n.Repr; + { + if (n == null) { + r := new Node.Init(x); + pos := 0; + } else if (x < n.data) { + var left; + assert n.left != null ==> n.data == n.Contents[|n.left.Contents|]; + assert n.left == null ==> n.data == n.Contents[0]; + left, pos := FunctionalInsert(n.left, x); + assert n.left == old(n.left); + if (left == n.left) { + r, pos := n, -1; + } else { + assert n.left != null ==> forall i :: 0 <= i < |n.left.Contents| ==> n.Contents[i] < n.data; + assert forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < n.data; + r := new Node.Build(left, n.data, n.right); + } + } else if (n.data < x) { + var right; + assert n.left != null ==> n.data == n.Contents[|n.left.Contents|]; + assert n.left == null ==> n.data == n.Contents[0]; + right, pos := FunctionalInsert(n.right, x); + if (right == n.right) { + assert n != null && x in n.Contents; + r, pos := n, -1; + } else { + assert n.left != null ==> forall i :: 0 <= i < |n.left.Contents| ==> n.left.Contents[i] < n.data; + assert forall i :: 0 <= i < |right.Contents| ==> n.data < right.Contents[i]; + r := new Node.Build(n.left, n.data, right); + pos := pos + 1 + if n.left == null then 0 else |n.left.Contents|; + assert n != null && x !in n.Contents ==> r.Contents == n.Contents[..pos] + [x] + n.Contents[pos..]; + } + } else { + r, pos := n, -1; + } + } + + method MutatingInsert(x: int) returns (ghost pos: int) + requires Valid(); + modifies Repr; + ensures Valid() && fresh(Repr - old(Repr)); + ensures x in old(Contents) ==> pos < 0 && Contents == old(Contents); + ensures x !in old(Contents) ==> + 0 <= pos < |Contents| == |old(Contents)| + 1 && + Contents == old(Contents[..pos] + [x] + Contents[pos..]); + decreases Repr; + { + assert data == Contents[if left==null then 0 else |left.Contents|]; + if (x < data) { + assert right == null || x !in right.Contents; + assert right != null ==> forall i :: 0 <= i < |right.Contents| ==> x < right.Contents[i]; + if (left == null) { + left := new Node.Init(x); + pos := 0; + } else { + assert forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < data; + pos := left.MutatingInsert(x); + assert Tree.IsSorted(left.Contents); + assert right != null ==> Tree.IsSorted(right.Contents); + assert forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < data; + } + Repr := Repr + left.Repr; + Contents := left.Contents + [data] + if right == null then [] else right.Contents; + assert Tree.IsSorted(Contents); + } else if (data < x) { + assert left == null || x !in left.Contents; + assert left != null ==> forall i :: 0 <= i < |left.Contents| ==> left.Contents[i] < x; + if (right == null) { + right := new Node.Init(x); + pos := 1 + if left == null then 0 else |left.Contents|; + } else { + assert forall i :: 0 <= i < |right.Contents| ==> data < right.Contents[i]; + pos := right.MutatingInsert(x); + assert Tree.IsSorted(right.Contents); + assert left != null ==> Tree.IsSorted(left.Contents); + assert forall i :: 0 <= i < |right.Contents| ==> data < right.Contents[i]; + if (0 <= pos) { + pos := pos + 1 + if left == null then 0 else |left.Contents|; + assert (if left == null then [] else left.Contents) + [data] + right.Contents == old(Contents[..pos] + [x] + Contents[pos..]); + } + } + Repr := Repr + right.Repr; + Contents := (if left == null then [] else left.Contents) + [data] + right.Contents; + assert Tree.IsSorted(Contents); + } else { + pos := -1; + } + } +} + +class Iterator +{ + // public + ghost var IterRepr: set; // note, IterRepr does not include T.Repr + ghost var Contents: seq; + ghost var N: int; + var T: Tree; + // private + var initialized: bool; + var stack: List; + + function Valid(): bool + reads this, IterRepr, T, T.Repr; + { + this in IterRepr && null !in IterRepr && + T != null && T.Valid() && IterRepr !! T.Repr && + Contents == T.Contents && -1 <= N <= |Contents| && + (initialized <==> 0 <= N) && + (N < 0 ==> R(stack, 0, Contents, T.Repr)) && + (0 <= N ==> R(stack, N, Contents, T.Repr)) + } + + // R(wlist, n, C, Nodes) says that C[n..] are data items yet to be processed. + // In more detail, wlist is a stack of tree fragments, where the concatenation of the + // "load" of each tree fragment (from the top of the stack downwards) equals + // C[n..]. A tree fragment is either + // * for Nil, the empty fragment + // * for Cons(p, rest), fragment [p.data]+p.right.Contents + // In each case, R(wlist,n,C,Nodes) implies that the fragment wlist proper is a prefix of C[n..]. + // Nodes is (an overapproximation of) the set of nodes read by R. + static function R(wlist: List, n: int, C: seq, Nodes: set): bool + reads Nodes; + decreases wlist; + { + match wlist + case Nil => n == |C| + case Cons(p, rest) => + p != null && p in Nodes && p.Repr <= Nodes && p.Valid() && + 0 <= n < |C| && p.data == C[n] && + R(rest, n + 1 + if p.right==null then 0 else |p.right.Contents|, C, Nodes) && + p.Contents[if p.left==null then 0 else |p.left.Contents| ..] <= C[n..] + } + + constructor Init(t: Tree) + requires t != null && t.Valid() && this !in t.Repr; + modifies this; + ensures Valid() && fresh(IterRepr - {this}); + ensures T == t && Contents == t.Contents && N == -1; + { + T := t; + IterRepr := {this}; + Contents := T.Contents; + initialized, stack, N := false, Nil, -1; + if (t.root != null) { + stack := Push(stack, 0, t.root, Contents, T.Repr); + } + } + + // private + static method Push(stIn: List, ghost n: int, p: Node, ghost C: seq, ghost Nodes: set) returns (st: List) + requires p != null && p in Nodes && p.Repr <= Nodes && p.Valid(); + requires 0 <= n <= |C|; + requires p.Contents <= C[n..]; + requires R(stIn, n + |p.Contents|, C, Nodes); + ensures R(st, n, C, Nodes); + decreases p.Contents; + { + st := Cons(p, stIn); + + assert p.data == p.Contents[if p.left == null then 0 else |p.left.Contents|]; // lemma + if (p.left != null) { + st := Push(st, n, p.left, C, Nodes); + } + } + + method Current() returns (x: int) + requires Valid() && 0 <= N < |Contents|; + ensures x == Contents[N]; + { + match (stack) { + case Cons(y, rest) => x := y.data; + } + } + + method MoveNext() returns (hasCurrent: bool) + requires Valid() && N <= |Contents|; + modifies IterRepr; + ensures Valid() && fresh(IterRepr - old(IterRepr)) && T.Repr == old(T.Repr); + ensures Contents == old(Contents) && T == old(T); + ensures old(N) < |Contents| ==> N == old(N) + 1; + ensures old(N) == |Contents| ==> N == old(N); + ensures hasCurrent <==> 0 <= N < |Contents|; + { + if (!initialized) { + initialized, N := true, 0; + hasCurrent := stack != Nil; + } else { + match (stack) { + case Nil => + hasCurrent := false; + case Cons(p, rest) => + // lemmas: + assert R(rest, N + 1 + if p.right==null then 0 else |p.right.Contents|, Contents, T.Repr); + ghost var k := if p.left==null then 0 else |p.left.Contents|; + assert p.Contents[k..] == [p.data] + p.Contents[k+1..]; + assert p.Contents[k+1..] <= Contents[N+1..]; + + stack, N := rest, N+1; + + if (p.right != null) { + stack := Push(stack, N, p.right, Contents, T.Repr); + } + hasCurrent := stack != Nil; + } + } + match (stack) { case Nil => assert N == |Contents|; case Cons(p, rest) => assert N < |Contents|; } // lemma + } +} + +datatype List = Nil | Cons(Node, List); + +/* The following method shows the problem of concurrent modifications and shows that the + * design of the snapshotable trees herein handle this correctly. That is, after inserting + * into a tree that is being iterated, use of the associated iterator can no longer be + * proved to be correct. + * +method TestConcurrentModification(t: Tree) + requires t != null && t.Valid() && !t.IsReadonly; + modifies t.MutableRepr; +{ + var it := t.CreateIterator(); + var more := it.MoveNext(); + if (more) { + var pos := t.Insert(52); // this modification of the collection renders all associated iterators invalid + more := it.MoveNext(); // error: operation t.Insert may have made this iterator invalid + } +} +*/ diff --git a/Test/dafny2/unsupported/lit.local.cfg b/Test/dafny2/unsupported/lit.local.cfg new file mode 100644 index 00000000..c4c53257 --- /dev/null +++ b/Test/dafny2/unsupported/lit.local.cfg @@ -0,0 +1,2 @@ +# Do not run tests in this directory and below +config.unsupported = True -- cgit v1.2.3 From 39a8abe0d2d6e4bda54fb3a481b049c19fe1dba9 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 1 Jul 2014 17:52:52 +0200 Subject: Removed the old test infrastructure. --- Test/Makefile | 17 - Test/VSComp2010/Answer | 20 - Test/VSComp2010/runtest.bat | 15 - Test/VSI-Benchmarks/Answer | 32 - Test/VSI-Benchmarks/runtest.bat | 13 - Test/alltests.txt | 10 - Test/cloudmake/Answer | 12 - Test/cloudmake/runtest.bat | 7 - Test/dafny0/Answer | 2616 ------------------------------------- Test/dafny0/runtest.bat | 61 - Test/dafny1/Answer | 124 -- Test/dafny1/runtest.bat | 26 - Test/dafny2/Answer | 60 - Test/dafny2/runtest.bat | 27 - Test/dafny3/Answer | 64 - Test/dafny3/runtest.bat | 19 - Test/dafny4/Answer | 43 - Test/dafny4/runtest.bat | 7 - Test/runtest.bat | 39 - Test/runtestall.bat | 24 - Test/vacid0/Answer | 12 - Test/vacid0/AnswerRuntimeChecking | 0 Test/vacid0/runtest.bat | 13 - Test/vstte2012/Answer | 24 - Test/vstte2012/runtest.bat | 23 - 25 files changed, 3308 deletions(-) delete mode 100644 Test/Makefile delete mode 100644 Test/VSComp2010/Answer delete mode 100644 Test/VSComp2010/runtest.bat delete mode 100644 Test/VSI-Benchmarks/Answer delete mode 100644 Test/VSI-Benchmarks/runtest.bat delete mode 100644 Test/alltests.txt delete mode 100644 Test/cloudmake/Answer delete mode 100644 Test/cloudmake/runtest.bat delete mode 100644 Test/dafny0/Answer delete mode 100644 Test/dafny0/runtest.bat delete mode 100644 Test/dafny1/Answer delete mode 100644 Test/dafny1/runtest.bat delete mode 100644 Test/dafny2/Answer delete mode 100644 Test/dafny2/runtest.bat delete mode 100644 Test/dafny3/Answer delete mode 100644 Test/dafny3/runtest.bat delete mode 100644 Test/dafny4/Answer delete mode 100644 Test/dafny4/runtest.bat delete mode 100644 Test/runtest.bat delete mode 100644 Test/runtestall.bat delete mode 100644 Test/vacid0/Answer delete mode 100644 Test/vacid0/AnswerRuntimeChecking delete mode 100644 Test/vacid0/runtest.bat delete mode 100644 Test/vstte2012/Answer delete mode 100644 Test/vstte2012/runtest.bat (limited to 'Test/dafny2') diff --git a/Test/Makefile b/Test/Makefile deleted file mode 100644 index 6e02aed0..00000000 --- a/Test/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -TESTS_FILE = alltests.txt -LONG = $(shell awk '{ if (tolower($$2) ~ /^long$$/) print $$1 }' $(TESTS_FILE)) -NORMAL = $(shell awk '{ if (tolower($$2) ~ /^use$$/) print $$1 }' $(TESTS_FILE)) -TESTS = $(NORMAL) - -all: dafny - -dafny: $(addprefix rundfy-, $(TESTS)) - -rundfy-%: - @cmd /c "runtest.bat $* $(FLAGS)" || : - -long: - $(MAKE) TESTS="$(NORMAL) $(LONG)" all - -show: - @echo $(TESTS) diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer deleted file mode 100644 index ff491aa5..00000000 --- a/Test/VSComp2010/Answer +++ /dev/null @@ -1,20 +0,0 @@ - --------------------- Problem1-SumMax.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Problem2-Invert.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- Problem3-FindZero.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- Problem4-Queens.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- Problem5-DoubleEndedQueue.dfy -------------------- - -Dafny program verifier finished with 21 verified, 0 errors diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat deleted file mode 100644 index 2cfcdafb..00000000 --- a/Test/VSComp2010/runtest.bat +++ /dev/null @@ -1,15 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy Problem5-DoubleEndedQueue.dfy - -rem for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy -rem Problem3-FindZero.dfy Problem4-Queens.dfy -rem Problem5-DoubleEndedQueue.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer deleted file mode 100644 index 2a4587f4..00000000 --- a/Test/VSI-Benchmarks/Answer +++ /dev/null @@ -1,32 +0,0 @@ - --------------------- b1.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- b2.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- b3.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- b4.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- b5.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- b6.dfy -------------------- - -Dafny program verifier finished with 21 verified, 0 errors - --------------------- b7.dfy -------------------- - -Dafny program verifier finished with 23 verified, 0 errors - --------------------- b8.dfy -------------------- - -Dafny program verifier finished with 42 verified, 0 errors diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat deleted file mode 100644 index f950cf2a..00000000 --- a/Test/VSI-Benchmarks/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy - -rem for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/alltests.txt b/Test/alltests.txt deleted file mode 100644 index c586a561..00000000 --- a/Test/alltests.txt +++ /dev/null @@ -1,10 +0,0 @@ -dafny0 Use Dafny functionality tests -dafny1 Use Various Dafny examples -dafny2 Use More Dafny examples -dafny3 Use And more Dafny examples -dafny4 Use More, more, more! -cloudmake Use CloudMake formalization and proofs -VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges -vacid0 Use Dafny attempts to VACID Edition 0 benchmarks -vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition -VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer deleted file mode 100644 index 3758853e..00000000 --- a/Test/cloudmake/Answer +++ /dev/null @@ -1,12 +0,0 @@ - --------------------- CloudMake-ParallelBuilds.dfy -------------------- - -Dafny program verifier finished with 244 verified, 0 errors - --------------------- CloudMake-CachedBuilds.dfy -------------------- - -Dafny program verifier finished with 104 verified, 0 errors - --------------------- CloudMake-ConsistentBuilds.dfy -------------------- - -Dafny program verifier finished with 59 verified, 0 errors diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat deleted file mode 100644 index 8fc7ccbb..00000000 --- a/Test/cloudmake/runtest.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer deleted file mode 100644 index dc3f1eda..00000000 --- a/Test/dafny0/Answer +++ /dev/null @@ -1,2616 +0,0 @@ - --------------------- Simple.dfy -------------------- -// Simple.dfy - -class MyClass { - var x: int; - - method M(s: bool, lotsaObjects: set) - returns (t: object, u: set, v: seq>) - requires s; - modifies this, lotsaObjects; - ensures t == t; - ensures old(null) != this; - { - x := 12; - while x < 100 - invariant x <= 100; - { - x := x + 17; - if x % 20 == 3 { - x := this.x + 1; - } else { - this.x := x + 0; - } - t, u, v := M(true, lotsaObjects); - var to: MyClass; - to, u, v := this.M(true, lotsaObjects); - to, u, v := to.M(true, lotsaObjects); - assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10]; - } - } - - function F(x: int, y: int, h: WildData, k: WildData): WildData - { - if x < 0 then - h - else if x == 0 then - if if h == k then true else false then - h - else if y == 0 then - k - else - h - else - k - } -} - -datatype List = Nil | Cons(T, List) - -datatype WildData = Something | JustAboutAnything(bool, myName: set, int, WildData) | More(List) - -class C { - var w: WildData; - var list: List; -} - -lemma M(x: int) - ensures x < 8; -{ -} - -colemma M'(x': int) - ensures true; -{ -} - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- TypeTests.dfy -------------------- -TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D) -TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C) -TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int) -TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int) -TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool) -TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C) -TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int) -TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -TypeTests.dfy(56,6): Error: Duplicate local-variable name: z -TypeTests.dfy(58,6): Error: Duplicate local-variable name: x -TypeTests.dfy(61,8): Error: Duplicate local-variable name: x -TypeTests.dfy(64,6): Error: Duplicate local-variable name: y -TypeTests.dfy(70,11): Error: unresolved identifier: x -TypeTests.dfy(72,28): Error: unresolved identifier: z -TypeTests.dfy(73,29): Error: unresolved identifier: w1 -TypeTests.dfy(73,47): Error: unresolved identifier: w0 -TypeTests.dfy(76,28): Error: unresolved identifier: e -TypeTests.dfy(91,17): Error: member F in type C does not refer to a method -TypeTests.dfy(92,17): Error: a method called as an initialization method must not have any result arguments -TypeTests.dfy(101,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(103,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(105,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type -TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts -TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed -33 resolution/type errors detected in TypeTests.dfy - --------------------- NatTypes.dfy -------------------- -NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 -NatTypes.dfy(34,10): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - NatTypes.dfy(22,3): anon10_LoopHead - (0,0): anon10_LoopBody - NatTypes.dfy(22,3): anon11_Else - (0,0): anon12_Then -NatTypes.dfy(41,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -NatTypes.dfy(43,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -NatTypes.dfy(60,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -NatTypes.dfy(74,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -NatTypes.dfy(107,45): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - -Dafny program verifier finished with 15 verified, 9 errors - --------------------- RealTypes.dfy -------------------- -RealTypes.dfy(8,23): Error: assertion violation -Execution trace: - (0,0): anon0 -RealTypes.dfy(14,12): Error: possible division by zero -Execution trace: - (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else - (0,0): anon2 -RealTypes.dfy(14,20): Error: assertion violation -Execution trace: - (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else - (0,0): anon2 -RealTypes.dfy(22,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 6 verified, 4 errors - --------------------- Definedness.dfy -------------------- -Definedness.dfy(11,7): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Definedness.dfy(18,16): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(27,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(28,21): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Definedness.dfy(29,17): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(36,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(45,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(53,18): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(54,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(53,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(60,18): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(61,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(60,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(68,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(67,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(88,7): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(89,5): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 -Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Definedness.dfy(89,10): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(90,10): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 -Definedness.dfy(95,14): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(95,23): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(96,15): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(101,12): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(108,15): Error: possible division by zero -Execution trace: - Definedness.dfy(108,5): anon7_LoopHead - (0,0): anon7_LoopBody - Definedness.dfy(108,5): anon8_Else -Definedness.dfy(117,23): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(116,5): anon12_LoopHead - (0,0): anon12_LoopBody - (0,0): anon13_Then -Definedness.dfy(123,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(116,5): anon12_LoopHead - (0,0): anon12_LoopBody - Definedness.dfy(116,5): anon13_Else - (0,0): anon14_Then - Definedness.dfy(122,5): anon15_LoopHead - (0,0): anon15_LoopBody - (0,0): anon16_Then -Definedness.dfy(133,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(132,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(133,22): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(134,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(132,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(143,15): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(143,5): anon8_LoopHead - (0,0): anon8_LoopBody - Definedness.dfy(143,5): anon9_Else -Definedness.dfy(162,15): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(156,5): anon16_LoopHead - (0,0): anon16_LoopBody - Definedness.dfy(156,5): anon17_Else - (0,0): anon18_Then - (0,0): anon5 - (0,0): anon19_Then - Definedness.dfy(162,5): anon20_LoopHead - (0,0): anon20_LoopBody - Definedness.dfy(162,5): anon21_Else -Definedness.dfy(175,28): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(181,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(173,5): anon18_LoopHead - (0,0): anon18_LoopBody - Definedness.dfy(173,5): anon19_Else - (0,0): anon20_Then - Definedness.dfy(180,5): anon21_LoopHead - (0,0): anon21_LoopBody - (0,0): anon22_Then - (0,0): anon23_Then - (0,0): anon11 -Definedness.dfy(196,19): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(194,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(196,23): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(196,28): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(194,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(217,46): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -Definedness.dfy(224,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(240,24): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon2 - (0,0): anon8_Else - -Dafny program verifier finished with 21 verified, 37 errors - --------------------- FunctionSpecifications.dfy -------------------- -FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else -FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon11_Else - (0,0): anon14_Else - (0,0): anon15_Then -FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon3 -FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -FunctionSpecifications.dfy(108,23): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(111,23): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(126,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -FunctionSpecifications.dfy(130,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(153,15): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(172,15): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Else -FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(160,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(188,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 19 verified, 17 errors - --------------------- ResolutionErrors.dfy -------------------- -ResolutionErrors.dfy(499,7): Error: RHS (of type List) not assignable to LHS (of type List) -ResolutionErrors.dfy(504,7): Error: RHS (of type List) not assignable to LHS (of type List) -ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>) -ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree -ResolutionErrors.dfy(565,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly -ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements -ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations -ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context -ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. -ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. -ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression -ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1) -ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object) -ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object) -ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object) -ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) -ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(429,2): Error: More than one default constructor -ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context -ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable -ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure -ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops -ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called -ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor -ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int) -ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3) -ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) -ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array) -ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name -ResolutionErrors.dfy(57,7): Error: unresolved identifier: F -ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name -ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance -ResolutionErrors.dfy(59,7): Error: unresolved identifier: G -ResolutionErrors.dfy(61,7): Error: unresolved identifier: M -ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance -ResolutionErrors.dfy(63,7): Error: unresolved identifier: N -ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters -ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global -ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') -ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') -ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') -ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') -ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1) -ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label -ResolutionErrors.dfy(263,2): Error: duplicate label -ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called -ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called -ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated -ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List) -ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int) -ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int) -ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts -ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass, got GenericClass) -ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) -ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool) -ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool) -ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(406,6): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint -ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(546,18): Error: unresolved identifier: w -ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses -ResolutionErrors.dfy(913,9): Error: unresolved identifier: s -135 resolution/type errors detected in ResolutionErrors.dfy - --------------------- ParseErrors.dfy -------------------- -ParseErrors.dfy(7,19): error: a chain cannot have more than one != operator -ParseErrors.dfy(9,37): error: this operator chain cannot continue with a descending operator -ParseErrors.dfy(10,38): error: this operator chain cannot continue with an ascending operator -ParseErrors.dfy(15,24): error: this operator chain cannot continue with a descending operator -ParseErrors.dfy(18,18): error: this operator cannot be part of a chain -ParseErrors.dfy(19,19): error: this operator cannot be part of a chain -ParseErrors.dfy(20,18): error: this operator cannot be part of a chain -ParseErrors.dfy(21,18): error: chaining not allowed from the previous operator -ParseErrors.dfy(49,8): error: the main operator of a calculation must be transitive -ParseErrors.dfy(65,2): error: this operator cannot continue this calculation -ParseErrors.dfy(66,2): error: this operator cannot continue this calculation -ParseErrors.dfy(71,2): error: this operator cannot continue this calculation -ParseErrors.dfy(72,2): error: this operator cannot continue this calculation -ParseErrors.dfy(78,2): error: this operator cannot continue this calculation -14 parse errors detected in ParseErrors.dfy - --------------------- Array.dfy -------------------- -Array.dfy(13,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(20,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Array.dfy(27,6): Error: index out of range -Execution trace: - (0,0): anon0 -Array.dfy(51,20): Error: assertion violation -Execution trace: - (0,0): anon0 -Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(66,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(110,21): Error: upper bound below lower bound or above length of array -Execution trace: - (0,0): anon0 - (0,0): anon14_Else - (0,0): anon18_Then - (0,0): anon19_Then - (0,0): anon20_Then - (0,0): anon11 -Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Then -Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(150,6): Error: insufficient reads clause to read array element -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Then -Array.dfy(158,6): Error: insufficient reads clause to read array element -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Then -Array.dfy(174,6): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Array.dfy(181,6): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Array.dfy(206,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(205,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(230,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(229,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(236,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(235,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(251,10): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(252,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then - -Dafny program verifier finished with 41 verified, 20 errors - --------------------- MultiDimArray.dfy -------------------- -MultiDimArray.dfy(56,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon12_Then -MultiDimArray.dfy(83,25): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - -Dafny program verifier finished with 8 verified, 2 errors - --------------------- NonGhostQuantifiers.dfy -------------------- -NonGhostQuantifiers.dfy(149,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(153,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(158,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(163,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c' -NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd' -NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i' -NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j' -NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j' -NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j' -NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y' -NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x' -NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -20 resolution/type errors detected in NonGhostQuantifiers.dfy - --------------------- AdvancedLHS.dfy -------------------- -AdvancedLHS.dfy(34,23): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon15_Else - -Dafny program verifier finished with 7 verified, 1 error - --------------------- ModulesCycle.dfy -------------------- -ModulesCycle.dfy(5,9): Error: module T does not exist -ModulesCycle.dfy(8,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B -2 resolution/type errors detected in ModulesCycle.dfy - --------------------- Modules0.dfy -------------------- -Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(13,7): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(14,8): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(56,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) -Modules0.dfy(57,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(68,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(75,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) -Modules0.dfy(75,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?) -Modules0.dfy(78,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?) -Modules0.dfy(83,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) -Modules0.dfy(92,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?) -Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) -Modules0.dfy(224,8): Error: new can be applied only to reference types (got X) -Modules0.dfy(233,13): Error: Undeclared type X in module B -Modules0.dfy(243,13): Error: unresolved identifier: X -Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X -Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?) -Modules0.dfy(283,12): Error: new can be applied only to reference types (got D) -Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(287,6): Error: expected method call, found expression -Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(288,6): Error: expected method call, found expression -Modules0.dfy(310,24): Error: module Q_Imp does not exist -Modules0.dfy(100,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) -28 resolution/type errors detected in Modules0.dfy - --------------------- Modules1.dfy -------------------- -Modules1.dfy(79,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Modules1.dfy(92,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Modules1.dfy(94,18): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0 -Execution trace: - (0,0): anon0 -Modules1.dfy(62,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 26 verified, 5 errors - --------------------- Modules2.dfy -------------------- -Modules2.dfy(46,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name) -Modules2.dfy(46,10): Error: new can be applied only to reference types (got C) -Modules2.dfy(49,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E') -Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B -Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B -5 resolution/type errors detected in Modules2.dfy - --------------------- BadFunction.dfy -------------------- -BadFunction.dfy(9,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 2 verified, 1 error - --------------------- Comprehensions.dfy -------------------- -Comprehensions.dfy(12,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon10_Then - (0,0): anon4 - (0,0): anon11_Then - (0,0): anon12_Then - (0,0): anon8 - -Dafny program verifier finished with 6 verified, 1 error - --------------------- Basics.dfy -------------------- -Basics.dfy(45,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Basics.dfy(69,42): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Then - (0,0): anon15_Then - Basics.dfy(69,72): anon16_Else - Basics.dfy(69,82): anon17_Else - Basics.dfy(69,95): anon18_Else - (0,0): anon12 -Basics.dfy(113,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 - (0,0): anon10_Then - (0,0): anon3 - (0,0): anon11_Then - (0,0): anon6 - (0,0): anon12_Then - (0,0): anon9 -Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 -Basics.dfy(158,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then -Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3 -Basics.dfy(160,10): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon3 -Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Then -Basics.dfy(176,15): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Else - (0,0): anon6 - (0,0): anon13_Then - (0,0): anon8 - (0,0): anon14_Then -Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 -Basics.dfy(429,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Basics.dfy(440,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -Basics.dfy(442,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 - -Dafny program verifier finished with 61 verified, 14 errors - --------------------- ControlStructures.dfy -------------------- -ControlStructures.dfy(8,3): Error: missing case in case statement: Purple -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -ControlStructures.dfy(8,3): Error: missing case in case statement: Blue -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Else - (0,0): anon9_Then -ControlStructures.dfy(17,3): Error: missing case in case statement: Purple -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -ControlStructures.dfy(46,5): Error: missing case in case statement: Red -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Else - (0,0): anon10_Then -ControlStructures.dfy(54,3): Error: missing case in case statement: Red -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Else - (0,0): anon10_Else - (0,0): anon11_Else - (0,0): anon12_Then -ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -ControlStructures.dfy(218,18): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - (0,0): anon71_Then -ControlStructures.dfy(235,21): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - ControlStructures.dfy(213,9): anon71_Else - (0,0): anon72_Then - (0,0): after_4 - ControlStructures.dfy(224,7): anon74_LoopHead - (0,0): anon74_LoopBody - ControlStructures.dfy(224,7): anon75_Else - ControlStructures.dfy(224,7): anon76_Else - (0,0): anon78_Then - (0,0): anon38 - (0,0): anon83_Then - (0,0): anon52 -ControlStructures.dfy(238,30): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon65_Then - (0,0): anon84_Then - (0,0): anon85_Then - (0,0): anon56 -ControlStructures.dfy(241,17): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - ControlStructures.dfy(213,9): anon71_Else - (0,0): anon72_Then - (0,0): after_4 - ControlStructures.dfy(224,7): anon74_LoopHead - (0,0): anon74_LoopBody - ControlStructures.dfy(224,7): anon75_Else - ControlStructures.dfy(224,7): anon76_Else - (0,0): anon79_Then - (0,0): anon82_Then - (0,0): anon86_Then - (0,0): anon58 - -Dafny program verifier finished with 22 verified, 10 errors - --------------------- Termination.dfy -------------------- -Termination.dfy(359,47): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Else -Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop -Execution trace: - (0,0): anon0 - Termination.dfy(108,3): anon6_LoopHead - (0,0): anon6_LoopBody - Termination.dfy(108,3): anon7_Else - Termination.dfy(108,3): anon8_Else -Termination.dfy(116,3): Error: cannot prove termination; try supplying a decreases clause for the loop -Execution trace: - (0,0): anon0 - Termination.dfy(116,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(116,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(116,3): anon11_Else -Termination.dfy(125,3): Error: decreases expression might not decrease -Execution trace: - (0,0): anon0 - Termination.dfy(125,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(125,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(125,3): anon11_Else -Termination.dfy(126,17): Error: decreases expression must be bounded below by 0 at end of loop iteration -Execution trace: - (0,0): anon0 - Termination.dfy(125,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(125,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(125,3): anon11_Else -Termination.dfy(254,35): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -Termination.dfy(294,3): Error: decreases expression might not decrease -Execution trace: - Termination.dfy(294,3): anon9_LoopHead - (0,0): anon9_LoopBody - Termination.dfy(294,3): anon10_Else - Termination.dfy(294,3): anon11_Else - (0,0): anon12_Else - -Dafny program verifier finished with 59 verified, 7 errors - --------------------- DTypes.dfy -------------------- -DTypes.dfy(18,14): Error: assertion violation -Execution trace: - (0,0): anon0 -DTypes.dfy(56,18): Error: assertion violation -Execution trace: - (0,0): anon0 -DTypes.dfy(120,13): Error: assertion violation -DTypes.dfy(92,30): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(126,13): Error: assertion violation -DTypes.dfy(92,20): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(136,12): Error: assertion violation -DTypes.dfy(131,6): Related location -DTypes.dfy(92,20): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(157,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon4 - -Dafny program verifier finished with 27 verified, 6 errors - --------------------- ParallelResolveErrors.dfy -------------------- -ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable -ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements -ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods -ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement -ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations -ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -21 resolution/type errors detected in ParallelResolveErrors.dfy - --------------------- Parallel.dfy -------------------- -Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold. -Parallel.dfy(60,14): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Then - (0,0): anon34_Then - (0,0): anon35_Then - (0,0): anon14 -Parallel.dfy(38,5): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon38_Then - (0,0): anon20 -Parallel.dfy(42,18): Error: possible violation of postcondition of forall statement -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Else - (0,0): anon39_Then - (0,0): anon40_Then - (0,0): anon26 -Parallel.dfy(47,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Else - (0,0): anon39_Then - (0,0): anon40_Then -Parallel.dfy(93,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon10_Else - (0,0): anon11_Then -Parallel.dfy(99,20): Error: possible violation of postcondition of forall statement -Execution trace: - (0,0): anon0 - (0,0): anon10_Else - (0,0): anon11_Then - (0,0): anon12_Then -Parallel.dfy(122,12): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - (0,0): anon7_Then - (0,0): anon3 -Parallel.dfy(185,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon19_Then - (0,0): anon20_Then - (0,0): anon5 -Parallel.dfy(296,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - -Dafny program verifier finished with 43 verified, 9 errors - --------------------- TypeParameters.dfy -------------------- -TypeParameters.dfy(47,22): Error: assertion violation -Execution trace: - (0,0): anon0 -TypeParameters.dfy(69,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -TypeParameters.dfy(156,12): Error: assertion violation -TypeParameters.dfy(156,28): Related location -Execution trace: - (0,0): anon0 - (0,0): anon20_Then - TypeParameters.dfy(156,32): anon21_Else - (0,0): anon5 -TypeParameters.dfy(158,12): Error: assertion violation -TypeParameters.dfy(158,33): Related location -Execution trace: - (0,0): anon0 - (0,0): anon23_Then - TypeParameters.dfy(158,37): anon24_Else - (0,0): anon11 -TypeParameters.dfy(160,12): Error: assertion violation -TypeParameters.dfy(160,20): Related location -Execution trace: - (0,0): anon0 - (0,0): anon25_Then -TypeParameters.dfy(162,12): Error: assertion violation -TypeParameters.dfy(147,5): Related location -TypeParameters.dfy(162,21): Related location -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -TypeParameters.dfy(164,12): Error: assertion violation -TypeParameters.dfy(149,8): Related location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then -TypeParameters.dfy(178,15): Error BP5005: This loop invariant might not be maintained by the loop. -TypeParameters.dfy(178,38): Related location -Execution trace: - (0,0): anon0 - TypeParameters.dfy(171,3): anon16_LoopHead - (0,0): anon16_LoopBody - TypeParameters.dfy(171,3): anon17_Else - (0,0): anon19_Then - TypeParameters.dfy(177,3): anon20_LoopHead - (0,0): anon20_LoopBody - TypeParameters.dfy(177,3): anon21_Else - TypeParameters.dfy(177,3): anon23_Else - -Dafny program verifier finished with 58 verified, 8 errors - --------------------- Datatypes.dfy -------------------- -Datatypes.dfy(297,10): Error BP5003: A postcondition might not hold on this return path. -Datatypes.dfy(295,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Else - (0,0): anon15_Then - (0,0): anon6 -Datatypes.dfy(298,12): Error: missing case in case statement: Appendix -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Else - (0,0): anon15_Else - (0,0): anon16_Then -Datatypes.dfy(349,5): Error: missing case in case statement: Cons -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then -Datatypes.dfy(349,5): Error: missing case in case statement: Nil -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -Datatypes.dfy(356,8): Error: missing case in case statement: Cons -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then -Datatypes.dfy(356,8): Error: missing case in case statement: Nil -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else - (0,0): anon12_Then -Datatypes.dfy(82,20): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon20_Else - (0,0): anon21_Then - (0,0): anon4 - (0,0): anon22_Else - (0,0): anon23_Then - (0,0): anon24_Else - (0,0): anon25_Then -Datatypes.dfy(170,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -Datatypes.dfy(172,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon5_Then -Datatypes.dfy(201,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons' -Execution trace: - (0,0): anon0 -Datatypes.dfy(204,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons' -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -Datatypes.dfy(225,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T'' -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - -Dafny program verifier finished with 44 verified, 12 errors - --------------------- StatementExpressions.dfy -------------------- -StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - (0,0): anon8_Then -StatementExpressions.dfy(59,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - StatementExpressions.dfy(53,7): anon8_Else -StatementExpressions.dfy(77,6): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - -Dafny program verifier finished with 17 verified, 5 errors - --------------------- Coinductive.dfy -------------------- -Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed -Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed -Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed -Coinductive.dfy(64,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed -Coinductive.dfy(93,8): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(94,8): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(95,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(95,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(101,5): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(104,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(105,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates -16 resolution/type errors detected in Coinductive.dfy - --------------------- Corecursion.dfy -------------------- -Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 20 verified, 8 errors - --------------------- CoResolution.dfy -------------------- -CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default -CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared# -CoResolution.dfy(21,7): Error: unresolved identifier: _k -CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) -CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause -CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause -CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -21 resolution/type errors detected in CoResolution.dfy - --------------------- CoPrefix.dfy -------------------- -CoPrefix.dfy(164,3): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(163,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -CoPrefix.dfy(169,3): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(168,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoPrefix.dfy(63,7): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Else - (0,0): anon9_Then -CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Else - (0,0): anon9_Then -CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold. -CoPrefix.dfy(101,17): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoPrefix.dfy(138,25): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon10_Then -CoPrefix.dfy(142,25): Error: assertion violation -CoPrefix.dfy(117,23): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon12_Then -CoPrefix.dfy(151,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(150,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 41 verified, 9 errors - --------------------- CoinductiveProofs.dfy -------------------- -CoinductiveProofs.dfy(29,12): Error: assertion violation -CoinductiveProofs.dfy(13,17): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(54,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(74,12): Error: assertion violation -CoinductiveProofs.dfy(54,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(80,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(100,12): Error: assertion violation -CoinductiveProofs.dfy(80,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(106,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - -Dafny program verifier finished with 35 verified, 8 errors - --------------------- TypeAntecedents.dfy -------------------- -TypeAntecedents.dfy(35,13): Error: assertion violation -Execution trace: - (0,0): anon0 -TypeAntecedents.dfy(58,1): Error BP5003: A postcondition might not hold on this return path. -TypeAntecedents.dfy(57,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon25_Then - (0,0): anon6 - (0,0): anon28_Then - (0,0): anon8 - (0,0): anon29_Else - (0,0): anon31_Else - (0,0): anon33_Then - (0,0): anon20 - (0,0): anon34_Then - (0,0): anon35_Then - (0,0): anon24 -TypeAntecedents.dfy(66,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon25_Else - (0,0): anon26_Then - (0,0): anon27_Else - -Dafny program verifier finished with 12 verified, 3 errors - --------------------- NoTypeArgs.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- EqualityTypes.dfy -------------------- -EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype -EqualityTypes.dfy(35,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality -EqualityTypes.dfy(40,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes a different number of type parameters -EqualityTypes.dfy(41,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters -EqualityTypes.dfy(45,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality -EqualityTypes.dfy(46,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality -EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) -EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) -EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) -EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D) -EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D) -11 resolution/type errors detected in EqualityTypes.dfy - --------------------- SplitExpr.dfy -------------------- -SplitExpr.dfy(92,15): Error: loop invariant violation -SplitExpr.dfy(86,44): Related location -Execution trace: - SplitExpr.dfy(91,3): anon7_LoopHead - -Dafny program verifier finished with 10 verified, 1 error - --------------------- LoopModifies.dfy -------------------- -LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(16,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(16,4): anon9_Else - LoopModifies.dfy(16,4): anon11_Else -LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(44,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(44,4): anon9_Else - LoopModifies.dfy(44,4): anon11_Else -LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(59,4): anon9_LoopHead - (0,0): anon9_LoopBody - LoopModifies.dfy(59,4): anon10_Else - LoopModifies.dfy(59,4): anon12_Else -LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause -Execution trace: - (0,0): anon0 -LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(92,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(92,4): anon9_Else - LoopModifies.dfy(92,4): anon11_Else -LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(136,4): anon17_LoopHead - (0,0): anon17_LoopBody - LoopModifies.dfy(136,4): anon18_Else - LoopModifies.dfy(136,4): anon20_Else - LoopModifies.dfy(141,7): anon21_LoopHead - (0,0): anon21_LoopBody - LoopModifies.dfy(141,7): anon22_Else - LoopModifies.dfy(141,7): anon24_Else -LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(195,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(195,4): anon9_Else - LoopModifies.dfy(195,4): anon11_Else -LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(275,4): anon16_LoopHead - (0,0): anon16_LoopBody - LoopModifies.dfy(275,4): anon17_Else - LoopModifies.dfy(275,4): anon19_Else - LoopModifies.dfy(283,7): anon20_LoopHead - (0,0): anon20_LoopBody - LoopModifies.dfy(283,7): anon21_Else - LoopModifies.dfy(283,7): anon23_Else - -Dafny program verifier finished with 23 verified, 9 errors - --------------------- Refinement.dfy -------------------- -Refinement.dfy(15,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(14,17): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(33,20): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy(64,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Refinement.dfy(74,17): Error: assertion violation -Execution trace: - (0,0): anon0 -Refinement.dfy(93,12): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(72,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Refinement.dfy(96,3): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(77,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy[IncorrectConcrete](115,15): Related location: This is the postcondition that might not hold. -Refinement.dfy(180,9): Related location -Execution trace: - (0,0): anon0 -Refinement.dfy(187,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy[IncorrectConcrete](123,15): Related location: This is the postcondition that might not hold. -Refinement.dfy(180,9): Related location -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Refinement.dfy(193,7): Error: assertion violation -Refinement.dfy[IncorrectConcrete](131,24): Related location -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 48 verified, 9 errors - --------------------- RefinementErrors.dfy -------------------- -RefinementErrors.dfy(30,17): Error: a refining method is not allowed to add preconditions -RefinementErrors.dfy(31,15): Error: a refining method is not allowed to extend the modifies clause -RefinementErrors.dfy(34,14): Error: a predicate declaration (abc) can only refine a predicate -RefinementErrors.dfy(35,8): Error: a field re-declaration (xyz) must be to ghostify the field -RefinementErrors.dfy(37,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F -RefinementErrors.dfy(38,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C') -RefinementErrors.dfy(38,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A') -RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B') -RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq' instead of 'set') -RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines -RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G -11 resolution/type errors detected in RefinementErrors.dfy - --------------------- ReturnErrors.dfy -------------------- -ReturnErrors.dfy(32,10): Error: cannot have method call in return statement. -ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement. -ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'. -3 resolution/type errors detected in ReturnErrors.dfy - --------------------- ReturnTests.dfy -------------------- - -Dafny program verifier finished with 20 verified, 0 errors - --------------------- ChainingDisjointTests.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- CallStmtTests.dfy -------------------- -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable -CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable -2 resolution/type errors detected in CallStmtTests.dfy - --------------------- MultiSets.dfy -------------------- -MultiSets.dfy(159,3): Error BP5003: A postcondition might not hold on this return path. -MultiSets.dfy(158,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MultiSets.dfy(165,3): Error BP5003: A postcondition might not hold on this return path. -MultiSets.dfy(164,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MultiSets.dfy(178,11): Error: new number of occurrences might be negative -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -MultiSets.dfy(269,24): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Then - (0,0): anon14_Else - -Dafny program verifier finished with 54 verified, 4 errors - --------------------- PredExpr.dfy -------------------- -PredExpr.dfy(7,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -PredExpr.dfy(52,17): Error: assertion violation -Execution trace: - (0,0): anon0 -PredExpr.dfy(77,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon3 - PredExpr.dfy(76,20): anon10_Else - (0,0): anon6 - -Dafny program verifier finished with 11 verified, 4 errors - --------------------- Predicates.dfy -------------------- -Predicates.dfy[B](21,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[B](20,15): Related location: This is the postcondition that might not hold. -Predicates.dfy(31,9): Related location -Execution trace: - (0,0): anon0 -Predicates.dfy(88,16): Error: assertion violation -Execution trace: - (0,0): anon0 -Predicates.dfy(92,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Predicates.dfy[Tricky_Full](126,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[Tricky_Full](125,15): Related location: This is the postcondition that might not hold. -Predicates.dfy(136,7): Related location -Predicates.dfy[Tricky_Full](116,9): Related location -Execution trace: - (0,0): anon0 -Predicates.dfy(164,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy(163,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Predicates.dfy[Q1](154,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[Q1](153,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 52 verified, 6 errors - --------------------- Skeletons.dfy -------------------- -Skeletons.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. -Skeletons.dfy(44,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - Skeletons.dfy[C0](32,5): anon11_LoopHead - (0,0): anon11_LoopBody - Skeletons.dfy[C0](32,5): anon12_Else - (0,0): anon13_Then - Skeletons.dfy[C0](37,19): anon15_Else - (0,0): anon10 - -Dafny program verifier finished with 9 verified, 1 error - --------------------- OpaqueFunctions.dfy -------------------- -OpaqueFunctions.dfy(27,16): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(58,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(60,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(63,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(66,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(77,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -OpaqueFunctions.dfy(86,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(88,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(91,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(94,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(105,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -OpaqueFunctions.dfy(114,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(116,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(119,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(122,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(138,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 43 verified, 19 errors - --------------------- Maps.dfy -------------------- -Maps.dfy(78,8): Error: element may not be in domain -Execution trace: - (0,0): anon0 -Maps.dfy(128,13): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 32 verified, 2 errors - --------------------- LiberalEquality.dfy -------------------- -LiberalEquality.dfy(20,14): Error: arguments must have the same type (got T and U) -LiberalEquality.dfy(39,14): Error: arguments must have the same type (got Weird and Weird) -LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array and array) -3 resolution/type errors detected in LiberalEquality.dfy - --------------------- RefinementModificationChecking.dfy -------------------- -RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously -RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously -2 resolution/type errors detected in RefinementModificationChecking.dfy - --------------------- TailCalls.dfy -------------------- -TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code -TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods -5 resolution/type errors detected in TailCalls.dfy - --------------------- IteratorResolution.dfy -------------------- -IteratorResolution.dfy(62,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(67,18): Error: arguments must have the same type (got _T0 and int) -IteratorResolution.dfy(79,19): Error: RHS (of type bool) not assignable to LHS (of type int) -IteratorResolution.dfy(82,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called -IteratorResolution.dfy(86,15): Error: logical negation expects a boolean argument (instead got int) -IteratorResolution.dfy(20,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(126,9): Error: unresolved identifier: _decreases3 -IteratorResolution.dfy(127,21): Error: arguments must have the same type (got int and ?) -IteratorResolution.dfy(128,2): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(135,9): Error: unresolved identifier: _decreases1 -IteratorResolution.dfy(140,9): Error: unresolved identifier: _decreases0 -12 resolution/type errors detected in IteratorResolution.dfy - --------------------- Iterators.dfy -------------------- -Iterators.dfy(251,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(274,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(284,24): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 -Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 -Iterators.dfy(343,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 -Iterators.dfy(370,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(103,22): Error: assertion violation -Execution trace: - (0,0): anon0 -Iterators.dfy(106,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Iterators.dfy(177,28): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon15_Then -Iterators.dfy(208,7): Error: an assignment to _new is only allowed to shrink the set -Execution trace: - (0,0): anon0 - Iterators.dfy(197,3): anon16_LoopHead - (0,0): anon16_LoopBody - Iterators.dfy(197,3): anon17_Else - Iterators.dfy(197,3): anon19_Else - (0,0): anon20_Then -Iterators.dfy(212,21): Error: assertion violation -Execution trace: - (0,0): anon0 - Iterators.dfy(197,3): anon16_LoopHead - (0,0): anon16_LoopBody - Iterators.dfy(197,3): anon17_Else - Iterators.dfy(197,3): anon19_Else - (0,0): anon21_Then -Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold. -Iterators.dfy(4,10): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon35_Then - (0,0): anon2 - (0,0): anon36_Then - (0,0): anon5 - (0,0): anon37_Then -Iterators.dfy(89,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Iterators.dfy(119,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Iterators.dfy(150,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold. -Iterators.dfy(125,10): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Iterators.dfy(234,14): Error: assertion violation -Execution trace: - (0,0): anon0 - Iterators.dfy(225,3): anon14_LoopHead - (0,0): anon14_LoopBody - Iterators.dfy(225,3): anon15_Else - Iterators.dfy(225,3): anon18_Else - (0,0): anon19_Else - -Dafny program verifier finished with 65 verified, 20 errors - --------------------- RankPos.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- RankNeg.dfy -------------------- -RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then - -Dafny program verifier finished with 1 verified, 4 errors - --------------------- Computations.dfy -------------------- - -Dafny program verifier finished with 58 verified, 0 errors - --------------------- ComputationsNeg.dfy -------------------- -ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path. -ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(23,1): Error BP5003: A postcondition might not hold on this return path. -ComputationsNeg.dfy(22,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(36,13): Error: assertion violation -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(45,13): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 7 verified, 5 errors - --------------------- Include.dfy -------------------- -Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(17,20): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Includee.dfy[Concrete](22,16): Error: assertion violation -Execution trace: - (0,0): anon0 -Include.dfy(27,7): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy[Concrete](20,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - -Dafny program verifier finished with 4 verified, 3 errors - --------------------- Includee.dfy -------------------- -Includee.dfy(21,3): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(20,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Includee.dfy(24,18): Error: assertion violation -Execution trace: - (0,0): anon0 -Includee.dfy(6,1): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(5,13): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 5 verified, 3 errors - --------------------- AutoReq.dfy -------------------- -AutoReq.dfy(247,3): Error: possible violation of function precondition -AutoReq.dfy(239,12): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(13,3): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(25,3): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(38,12): Error: assertion violation -AutoReq.dfy(31,13): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then -AutoReq.dfy(38,12): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then -AutoReq.dfy(40,12): Error: assertion violation -AutoReq.dfy(31,27): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -AutoReq.dfy(40,12): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -AutoReq.dfy(45,12): Error: assertion violation -AutoReq.dfy(31,13): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - -Dafny program verifier finished with 52 verified, 8 errors - --------------------- DatatypeUpdate.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ModifyStmt.dfy -------------------- -ModifyStmt.dfy(27,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(42,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(48,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(61,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(70,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(89,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - ModifyStmt.dfy(81,7): anon10_LoopHead - (0,0): anon10_LoopBody - ModifyStmt.dfy(81,7): anon11_Else - (0,0): anon12_Then - (0,0): anon8 -ModifyStmt.dfy(99,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(110,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(122,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -ModifyStmt.dfy(134,7): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(172,15): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 25 verified, 11 errors - --------------------- SeqSlice.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- RealCompare.dfy -------------------- -RealCompare.dfy(35,5): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0 -Execution trace: - (0,0): anon0 -RealCompare.dfy(141,12): Error: assertion violation -Execution trace: - (0,0): anon0 - RealCompare.dfy(133,3): anon7_LoopHead - (0,0): anon7_LoopBody - RealCompare.dfy(133,3): anon8_Else - (0,0): anon9_Then -RealCompare.dfy(156,12): Error: assertion violation -Execution trace: - (0,0): anon0 - RealCompare.dfy(147,3): anon9_LoopHead - (0,0): anon9_LoopBody - RealCompare.dfy(147,3): anon10_Else - (0,0): anon12_Then - -Dafny program verifier finished with 24 verified, 4 errors - --------------------- AssumptionVariables0.dfy -------------------- -AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && " -AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost -AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool' -AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " -AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " -AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost -AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool' -AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -13 resolution/type errors detected in AssumptionVariables0.dfy - --------------------- AssumptionVariables1.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Superposition.dfy -------------------- - -Verifying CheckWellformed$$_0_M0.C.M ... - [0 proof obligations] verified - -Verifying Impl$$_0_M0.C.M ... - [4 proof obligations] verified - -Verifying CheckWellformed$$_0_M0.C.P ... - [4 proof obligations] verified - -Verifying CheckWellformed$$_0_M0.C.Q ... - [3 proof obligations] error -Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy(28,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - -Verifying CheckWellformed$$_0_M0.C.R ... - [3 proof obligations] error -Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy(34,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - -Verifying CheckWellformed$$_1_M1.C.M ... - [0 proof obligations] verified - -Verifying Impl$$_1_M1.C.M ... - [1 proof obligation] verified - -Verifying CheckWellformed$$_1_M1.C.P ... - [1 proof obligation] error -Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon9_Then - (0,0): anon6 - -Verifying CheckWellformed$$_1_M1.C.Q ... - [0 proof obligations] verified - -Verifying CheckWellformed$$_1_M1.C.R ... - [0 proof obligations] verified - -Dafny program verifier finished with 7 verified, 3 errors - --------------------- SmallTests.dfy -------------------- -SmallTests.dfy(33,11): Error: index out of range -Execution trace: - (0,0): anon0 -SmallTests.dfy(64,36): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -SmallTests.dfy(65,51): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Else - (0,0): anon3 - (0,0): anon13_Else -SmallTests.dfy(66,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - (0,0): anon3 - (0,0): anon13_Then - (0,0): anon6 -SmallTests.dfy(85,24): Error: target object may be null -Execution trace: - (0,0): anon0 - SmallTests.dfy(84,5): anon8_LoopHead - (0,0): anon8_LoopBody - (0,0): anon9_Then -SmallTests.dfy(119,5): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon3 -SmallTests.dfy(132,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -SmallTests.dfy(134,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(174,9): Error: assignment may update an object field not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon22_Else - (0,0): anon24_Else - (0,0): anon26_Else - (0,0): anon28_Then - (0,0): anon29_Then - (0,0): anon19 -SmallTests.dfy(198,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -SmallTests.dfy(205,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Then -SmallTests.dfy(207,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Else -SmallTests.dfy(253,24): Error BP5002: A precondition for this call might not hold. -SmallTests.dfy(231,30): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - SmallTests.dfy(248,19): anon3_Else - (0,0): anon2 -SmallTests.dfy(358,12): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(368,12): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(378,6): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(682,14): Error: assertion violation -Execution trace: - (0,0): anon0 - SmallTests.dfy(679,5): anon7_LoopHead - (0,0): anon7_LoopBody - SmallTests.dfy(679,5): anon8_Else - (0,0): anon9_Then -SmallTests.dfy(703,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Then - (0,0): anon3 -SmallTests.dfy(288,3): Error BP5003: A postcondition might not hold on this return path. -SmallTests.dfy(282,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon18_Else - (0,0): anon23_Then - (0,0): anon24_Then - (0,0): anon15 - (0,0): anon25_Else -SmallTests.dfy(329,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon7 -SmallTests.dfy(336,10): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(346,4): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(390,10): Error BP5003: A postcondition might not hold on this return path. -SmallTests.dfy(393,41): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -SmallTests.dfy(553,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -SmallTests.dfy(567,20): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - (0,0): anon28_Then - (0,0): anon4 - (0,0): anon29_Then - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Then - (0,0): anon32_Then - (0,0): anon12 -SmallTests.dfy(569,15): Error: left-hand sides 1 and 2 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - SmallTests.dfy(562,18): anon28_Else - (0,0): anon4 - (0,0): anon29_Else - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Else - (0,0): anon35_Then - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon22 - (0,0): anon38_Then -SmallTests.dfy(576,25): Error: target object may be null -Execution trace: - (0,0): anon0 -SmallTests.dfy(589,10): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(613,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 -SmallTests.dfy(636,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Then - (0,0): anon4 - (0,0): anon10_Then - (0,0): anon7 -SmallTests.dfy(650,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon3 -SmallTests.dfy(652,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -SmallTests.dfy(665,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 87 verified, 33 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- LetExpr.dfy -------------------- -LetExpr.dfy(8,12): Error: assertion violation -Execution trace: - (0,0): anon0 -LetExpr.dfy(107,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then -LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -LetExpr.dfy(256,24): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -LetExpr.dfy(285,14): Error: RHS is not certain to look like the pattern 'Agnes' -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -LetExpr.dfy(302,42): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -LetExpr.dfy(304,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - -Dafny program verifier finished with 38 verified, 8 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- Calculations.dfy -------------------- -Calculations.dfy(6,6): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon24_Then -Calculations.dfy(11,15): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(11,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(55,12): Error: assertion violation -Execution trace: - (0,0): anon0 - Calculations.dfy(50,3): anon5_Else -Calculations.dfy(78,15): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -Calculations.dfy(78,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - -Dafny program verifier finished with 9 verified, 6 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- DirtyLoops.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - -Dafny program verifier finished with 0 verified, 0 errors - -Dafny program verifier finished with 44 verified, 0 errors -Compiled assembly into Compilation.exe - -Dafny program verifier finished with 15 verified, 0 errors -Compilation error: Arbitrary type ('_module.MyType') cannot be compiled -Compilation error: Iterator _module.Iter has no body -Compilation error: Method _module._default.M has no body -Compilation error: Method _module._default.P has no body -Compilation error: an assume statement cannot be compiled (line 11) -Compilation error: Function _module._default.F has no body -Compilation error: Function _module._default.H has no body -Compilation error: an assume statement cannot be compiled (line 20) -Compilation error: an assume statement cannot be compiled (line 23) -Compilation error: an assume statement cannot be compiled (line 28) -Compilation error: an assume statement cannot be compiled (line 37) diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat deleted file mode 100644 index 1a371ba3..00000000 --- a/Test/dafny0/runtest.bat +++ /dev/null @@ -1,61 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -for %%f in (Simple.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f -) - -for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy - FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy - Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy - ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy - Comprehensions.dfy Basics.dfy ControlStructures.dfy - Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy - TypeParameters.dfy Datatypes.dfy StatementExpressions.dfy - Coinductive.dfy Corecursion.dfy CoResolution.dfy - CoPrefix.dfy CoinductiveProofs.dfy - TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy - LoopModifies.dfy Refinement.dfy RefinementErrors.dfy - ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy - CallStmtTests.dfy MultiSets.dfy PredExpr.dfy - Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy - Maps.dfy LiberalEquality.dfy - RefinementModificationChecking.dfy TailCalls.dfy - IteratorResolution.dfy Iterators.dfy - RankPos.dfy RankNeg.dfy - Computations.dfy ComputationsNeg.dfy - Include.dfy Includee.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy - RealCompare.dfy - AssumptionVariables0.dfy AssumptionVariables1.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f -) - -for %%f in (Superposition.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f -) - -for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f - %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy -) - -for %%f in (DirtyLoops.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f - %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy -) - -%DAFNY_EXE% %* Compilation.dfy -%DAFNY_EXE% %* CompilationErrors.dfy diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer deleted file mode 100644 index e60451c2..00000000 --- a/Test/dafny1/Answer +++ /dev/null @@ -1,124 +0,0 @@ - --------------------- Queue.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- PriorityQueue.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- ExtensibleArray.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- ExtensibleArrayAuto.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- BinaryTree.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- UnboundedStack.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SeparationLogicList.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- ListCopy.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- ListReverse.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ListContents.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- MatrixFun.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- pow2.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- SchorrWaite.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- SchorrWaite-stages.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- Cubes.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- SumOfCubes.dfy -------------------- - -Dafny program verifier finished with 17 verified, 0 errors - --------------------- FindZero.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- TerminationDemos.dfy -------------------- - -Dafny program verifier finished with 14 verified, 0 errors - --------------------- Substitution.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- TreeDatatype.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- KatzManna.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Induction.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- Rippling.dfy -------------------- - -Dafny program verifier finished with 141 verified, 0 errors - --------------------- MoreInduction.dfy -------------------- -MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 15 verified, 4 errors - --------------------- Celebrity.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- BDD.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- UltraFilter.dfy -------------------- - -Dafny program verifier finished with 19 verified, 0 errors diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat deleted file mode 100644 index f02a7965..00000000 --- a/Test/dafny1/runtest.bat +++ /dev/null @@ -1,26 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy - -rem for %%f in (Queue.dfy PriorityQueue.dfy -rem ExtensibleArray.dfy ExtensibleArrayAuto.dfy -rem BinaryTree.dfy -rem UnboundedStack.dfy -rem SeparationLogicList.dfy -rem ListCopy.dfy ListReverse.dfy ListContents.dfy -rem MatrixFun.dfy pow2.dfy -rem SchorrWaite.dfy SchorrWaite-stages.dfy -rem Cubes.dfy SumOfCubes.dfy FindZero.dfy -rem TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy -rem Induction.dfy Rippling.dfy MoreInduction.dfy -rem Celebrity.dfy BDD.dfy -rem UltraFilter.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer deleted file mode 100644 index 9fa6f4ef..00000000 --- a/Test/dafny2/Answer +++ /dev/null @@ -1,60 +0,0 @@ - --------------------- Classics.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- TreeBarrier.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- COST-verif-comp-2011-1-MaxArray.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- COST-verif-comp-2011-2-MaxTree-class.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- COST-verif-comp-2011-2-MaxTree-datatype.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- COST-verif-comp-2011-3-TwoDuplicates.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy -------------------- - -Dafny program verifier finished with 25 verified, 0 errors - --------------------- StoreAndRetrieve.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- Intervals.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- TreeFill.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- TuringFactorial.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- MajorityVote.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- SegmentSum.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- MonotonicHeapstate.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors - --------------------- Calculations.dfy -------------------- - -Dafny program verifier finished with 31 verified, 0 errors diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat deleted file mode 100644 index d038acce..00000000 --- a/Test/dafny2/runtest.bat +++ /dev/null @@ -1,27 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -REM soon again: SnapshotableTrees.dfy - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Classics.dfy TreeBarrier.dfy COST-verif-comp-2011-1-MaxArray.dfy COST-verif-comp-2011-2-MaxTree-class.dfy COST-verif-comp-2011-2-MaxTree-datatype.dfy COST-verif-comp-2011-3-TwoDuplicates.dfy COST-verif-comp-2011-4-FloydCycleDetect.dfy StoreAndRetrieve.dfy Intervals.dfy TreeFill.dfy TuringFactorial.dfy MajorityVote.dfy SegmentSum.dfy MonotonicHeapstate.dfy Calculations.dfy - -rem for %%f in ( -rem Classics.dfy -rem TreeBarrier.dfy -rem COST-verif-comp-2011-1-MaxArray.dfy -rem COST-verif-comp-2011-2-MaxTree-class.dfy -rem COST-verif-comp-2011-2-MaxTree-datatype.dfy -rem COST-verif-comp-2011-3-TwoDuplicates.dfy -rem COST-verif-comp-2011-4-FloydCycleDetect.dfy -rem StoreAndRetrieve.dfy -rem Intervals.dfy TreeFill.dfy TuringFactorial.dfy -rem MajorityVote.dfy SegmentSum.dfy -rem MonotonicHeapstate.dfy Calculations.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer deleted file mode 100644 index 9e8ac835..00000000 --- a/Test/dafny3/Answer +++ /dev/null @@ -1,64 +0,0 @@ - --------------------- Iter.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- Streams.dfy -------------------- - -Dafny program verifier finished with 52 verified, 0 errors - --------------------- Dijkstra.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- CachedContainer.dfy -------------------- - -Dafny program verifier finished with 47 verified, 0 errors - --------------------- SimpleInduction.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SimpleCoinduction.dfy -------------------- - -Dafny program verifier finished with 31 verified, 0 errors - --------------------- CalcExample.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- InductionVsCoinduction.dfy -------------------- - -Dafny program verifier finished with 20 verified, 0 errors - --------------------- Zip.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- SetIterations.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- Paulson.dfy -------------------- - -Dafny program verifier finished with 28 verified, 0 errors - --------------------- Filter.dfy -------------------- - -Dafny program verifier finished with 43 verified, 0 errors - --------------------- WideTrees.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- InfiniteTrees.dfy -------------------- - -Dafny program verifier finished with 88 verified, 0 errors - --------------------- OpaqueTrees.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- GenericSort.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat deleted file mode 100644 index 41971d4e..00000000 --- a/Test/dafny3/runtest.bat +++ /dev/null @@ -1,19 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy GenericSort.dfy - -rem for %%f in ( -rem Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy -rem SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy -rem InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy -rem Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy -rem OpaqueTrees.dfy GenericSort.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer deleted file mode 100644 index 14986a59..00000000 --- a/Test/dafny4/Answer +++ /dev/null @@ -1,43 +0,0 @@ - --------------------- CoqArt-InsertionSort.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors - --------------------- GHC-MergeSort.dfy -------------------- - -Dafny program verifier finished with 83 verified, 0 errors - --------------------- Fstar-QuickSort.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Primes.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- KozenSilva.dfy -------------------- - -Dafny program verifier finished with 47 verified, 0 errors - --------------------- SoftwareFoundations-Basics.dfy -------------------- -SoftwareFoundations-Basics.dfy(41,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 82 verified, 1 error - --------------------- NumberRepresentations.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- Circ.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- ACL2-extractor.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- ClassRefinement.dfy -------------------- - -Dafny program verifier finished with 18 verified, 0 errors diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat deleted file mode 100644 index cec5d271..00000000 --- a/Test/dafny4/runtest.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy ACL2-extractor.dfy ClassRefinement.dfy diff --git a/Test/runtest.bat b/Test/runtest.bat deleted file mode 100644 index dfc3ae00..00000000 --- a/Test/runtest.bat +++ /dev/null @@ -1,39 +0,0 @@ -@echo off -rem Usage: runtest.bat -if "%1" == "" goto noDirSpecified -if not exist %1\nul goto noDirExists -echo ----- Running regression test %1 -pushd %1 -if not exist runtest.bat goto noRunTest -call runtest.bat -nologo -logPrefix:%* > Output -rem There seem to be some race between finishing writing to the Output file, and running fc. -rem Calling fc twice seems to fix (or at least alleviate) the problem. -fc /W Answer Output > nul -fc /W Answer Output > nul -if not errorlevel 1 goto passTest -echo ============ %1 FAILED ==================================== -goto errorEnd - -:passTest -echo Success: %1 -goto end - -:noDirSpecified -echo runtest: Error: Syntax: runtest testDirectory [ additionalTestArguments ... ] -goto errorEnd - -:noDirExists -echo runtest: Error: There is no test directory %1 -goto errorEnd - -:noRunTest -echo runtest: Error: no runtest.bat found in test directory %1 -goto errorEnd - -:errorEnd -popd -exit /b 1 - -:end -popd -exit /b 0 diff --git a/Test/runtestall.bat b/Test/runtestall.bat deleted file mode 100644 index 207bb030..00000000 --- a/Test/runtestall.bat +++ /dev/null @@ -1,24 +0,0 @@ -@echo off -setlocal - -set errors=0 - -if "%1" == "short" goto UseShort - -set IncludeLong=True -goto Loop - -:UseShort -set IncludeLong=False -shift -goto Loop - -:Loop -for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1 - -if not %IncludeLong%==True goto End - -for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Long call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1 - -:End -exit /b %errors% \ No newline at end of file diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer deleted file mode 100644 index 90bbcc78..00000000 --- a/Test/vacid0/Answer +++ /dev/null @@ -1,12 +0,0 @@ - --------------------- LazyInitArray.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- SparseArray.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- Composite.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking deleted file mode 100644 index e69de29b..00000000 diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat deleted file mode 100644 index d7f31c3b..00000000 --- a/Test/vacid0/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* LazyInitArray.dfy SparseArray.dfy Composite.dfy - -rem for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer deleted file mode 100644 index 43eddcb1..00000000 --- a/Test/vstte2012/Answer +++ /dev/null @@ -1,24 +0,0 @@ - --------------------- Two-Way-Sort.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Combinators.dfy -------------------- - -Dafny program verifier finished with 25 verified, 0 errors - --------------------- RingBuffer.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- RingBufferAuto.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- Tree.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- BreadthFirstSearch.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat deleted file mode 100644 index 7e597fd4..00000000 --- a/Test/vstte2012/runtest.bat +++ /dev/null @@ -1,23 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy - -echo. -echo -------------------- BreadthFirstSearch.dfy -------------------- -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /vcsMaxKeepGoingSplits:10 %* BreadthFirstSearch.dfy - -rem for %%f in ( -rem Two-Way-Sort.dfy -rem Combinators.dfy -rem RingBuffer.dfy RingBufferAuto.dfy -rem Tree.dfy -rem BreadthFirstSearch.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) -- cgit v1.2.3