Skip to content

Commit

Permalink
Fixed the test provenance
Browse files Browse the repository at this point in the history
  • Loading branch information
@MikaelMayer
MikaelMayer committed Apr 11, 2022
1 parent 361e48a commit acaaff0
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 44 deletions.
26 changes: 13 additions & 13 deletions Test/git-issues/git-issue-1604b2.dfy.expect
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
git-issue-1604e.dfy(65,37): Error: Could not prove that the range constrains the bound variable 'go' to be of type GhostOrdinalCell, and since GhostOrdinalCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(24,24): [Related location] The subset type GhostOrdinalCelltype GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell
git-issue-1604e.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(65,103): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell'
git-issue-1604e.dfy(67,37): Error: Could not prove that the range constrains the bound variable 'go2' to be of type GhostOrdinalCell2, and since GhostOrdinalCell2 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type CompilableNaturalCell.
git-issue-1604e.dfy(26,55): [Related location] GhostOrdinalCell2 is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(67,37): Error: value does not satisfy the subset constraints of 'set<GhostOrdinalCell>'
git-issue-1604e.dfy(67,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell'
git-issue-1604e.dfy(69,37): Error: Could not prove that the range constrains the bound variable 'go3' to be of type GhostOrdinalCell3, and since GhostOrdinalCell3 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(28,25): [Related location] The subset type GhostOrdinalCell3type GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell
git-issue-1604e.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(69,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell'
git-issue-1604e.dfy(71,9): Error: assertion might not hold
git-issue-1604b2.dfy(65,37): Error: Could not prove that the range constrains the bound variable 'go' to be of type GhostOrdinalCell, and since GhostOrdinalCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604b2.dfy(24,24): [Related location] The subset type GhostOrdinalCelltype GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell
git-issue-1604b2.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b2.dfy(65,103): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell'
git-issue-1604b2.dfy(67,37): Error: Could not prove that the range constrains the bound variable 'go2' to be of type GhostOrdinalCell2, and since GhostOrdinalCell2 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type CompilableNaturalCell.
git-issue-1604b2.dfy(26,55): [Related location] GhostOrdinalCell2 is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b2.dfy(67,37): Error: value does not satisfy the subset constraints of 'set<GhostOrdinalCell>'
git-issue-1604b2.dfy(67,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell'
git-issue-1604b2.dfy(69,37): Error: Could not prove that the range constrains the bound variable 'go3' to be of type GhostOrdinalCell3, and since GhostOrdinalCell3 is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604b2.dfy(28,25): [Related location] The subset type GhostOrdinalCell3type GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell
git-issue-1604b2.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b2.dfy(69,106): Error: value does not satisfy the subset constraints of 'GhostOrdinalCell'
git-issue-1604b2.dfy(71,9): Error: assertion might not hold

Dafny program verifier finished with 12 verified, 8 errors
26 changes: 13 additions & 13 deletions Test/git-issues/git-issue-1604e.dfy.expect
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
git-issue-1604b.dfy(54,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b.dfy(54,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604b.dfy(57,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b.dfy(60,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b.dfy(63,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604b.dfy(66,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604b.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604b.dfy(66,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604b.dfy(69,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604b.dfy(71,9): Error: assertion might not hold
git-issue-1604e.dfy(54,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(54,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604e.dfy(57,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(60,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(63,77): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604e.dfy(66,34): Error: Could not prove that the range constrains the bound variable 'c' to be of type GhostEvenCell, and since GhostEvenCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(10,31): [Related location] GhostEvenCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604e.dfy(66,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604e.dfy(69,92): Error: value does not satisfy the subset constraints of 'GhostEvenCell'
git-issue-1604e.dfy(71,9): Error: assertion might not hold

Dafny program verifier finished with 9 verified, 9 errors
36 changes: 18 additions & 18 deletions Test/git-issues/git-issue-1604g.dfy.expect
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
git-issue-1604f.dfy(38,8): Error: Could not prove that the range constrains the bound variable 'f' to be of type SpecialFruit, and since SpecialFruit is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Fruit.
git-issue-1604f.dfy(16,31): [Related location] SpecialFruit is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604f.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604f.dfy(19,11): Related location
git-issue-1604f.dfy(13,2): Related location
git-issue-1604f.dfy(8,25): Related location
git-issue-1604f.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604f.dfy(19,11): Related location
git-issue-1604f.dfy(13,2): Related location
git-issue-1604f.dfy(9,19): Related location
git-issue-1604f.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604f.dfy(19,11): Related location
git-issue-1604f.dfy(13,2): Related location
git-issue-1604f.dfy(8,25): Related location
git-issue-1604f.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604f.dfy(19,11): Related location
git-issue-1604f.dfy(13,2): Related location
git-issue-1604f.dfy(9,19): Related location
git-issue-1604g.dfy(38,8): Error: Could not prove that the range constrains the bound variable 'f' to be of type SpecialFruit, and since SpecialFruit is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Fruit.
git-issue-1604g.dfy(16,31): [Related location] SpecialFruit is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
git-issue-1604g.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604g.dfy(19,11): Related location
git-issue-1604g.dfy(13,2): Related location
git-issue-1604g.dfy(8,25): Related location
git-issue-1604g.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604g.dfy(19,11): Related location
git-issue-1604g.dfy(13,2): Related location
git-issue-1604g.dfy(9,19): Related location
git-issue-1604g.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604g.dfy(19,11): Related location
git-issue-1604g.dfy(13,2): Related location
git-issue-1604g.dfy(8,25): Related location
git-issue-1604g.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
git-issue-1604g.dfy(19,11): Related location
git-issue-1604g.dfy(13,2): Related location
git-issue-1604g.dfy(9,19): Related location

Dafny program verifier finished with 4 verified, 5 errors

0 comments on commit acaaff0

Please sign in to comment.