start ------ Running regression test AssociationList.chalice Boogie program verifier finished with 12 verified, 0 errors ------ Running regression test cell.chalice 142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid. Boogie program verifier finished with 31 verified, 1 error ------ Running regression test counter.chalice 69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true. 80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true. 119.5: The held field of the target of the release statement might not be writable. 128.7: The mu field of the target of the acquire statement might not be above maxlock. 136.7: The mu field of the target of the acquire statement might not be above maxlock. 145.5: The held field of the target of the release statement might not be writable. Boogie program verifier finished with 24 verified, 6 errors ------ Running regression test dining-philosophers.chalice Boogie program verifier finished with 12 verified, 0 errors ------ Running regression test ForkJoin.chalice Boogie program verifier finished with 18 verified, 0 errors ------ Running regression test HandOverHand.chalice Boogie program verifier finished with 10 verified, 0 errors ------ Running regression test iterator.chalice Boogie program verifier finished with 22 verified, 0 errors ------ Running regression test iterator2.chalice Boogie program verifier finished with 21 verified, 0 errors ------ Running regression test producer-consumer.chalice Boogie program verifier finished with 36 verified, 0 errors ------ Running regression test prog0.chalice The program did not typecheck. 3.17: undeclared member a in class C 3.37: undeclared member a in class C 3.41: undeclared member a in class C 3.12: assert statement requires a boolean expression (found int) 4.5: undeclared member a in class C 4.10: undeclared member a in class C 5.5: undeclared member b in class C 5.10: undeclared member a in class C 5.14: undeclared member b in class C 5.18: undeclared member c in class C 5.26: undeclared member d in class C 6.5: undeclared member b in class C 6.14: undeclared member a in class C 6.18: undeclared member b in class C 6.23: undeclared member c in class C 6.32: undeclared member d in class C 7.5: undeclared member c in class C 7.10: undeclared member a in class C 7.15: undeclared member b in class C 7.20: undeclared member c in class C 7.29: undeclared member d in class C 8.13: undeclared member X in class C 8.19: undeclared member Y in class C 8.13: incorrect type of ==> LHS (expected bool, found int) 8.19: incorrect type of ==> RHS (expected bool, found int) 8.26: undeclared member Z in class C 8.26: incorrect type of ==> RHS (expected bool, found int) 8.33: undeclared member A in class C 8.39: undeclared member B in class C 8.45: undeclared member C in class C 8.39: incorrect type of ==> LHS (expected bool, found int) 8.45: incorrect type of ==> RHS (expected bool, found int) 8.33: incorrect type of ==> LHS (expected bool, found int) 9.12: undeclared member A in class C 9.17: undeclared member B in class C 9.12: incorrect type of && LHS (expected bool, found int) 9.17: incorrect type of && RHS (expected bool, found int) 9.23: undeclared member C in class C 9.28: undeclared member D in class C 9.23: incorrect type of || LHS (expected bool, found int) 9.28: incorrect type of || RHS (expected bool, found int) 9.33: undeclared member E in class C 9.33: incorrect type of || RHS (expected bool, found int) 9.39: undeclared member F in class C 9.39: incorrect type of && RHS (expected bool, found int) 11.21: undeclared member f in class int 11.21: undeclared member g in class int 11.21: undeclared member h in class int : not-expression requires boolean operand : incorrect type of + RHS (expected int, found bool) 11.33: not-expression requires boolean operand 11.33: undeclared member f in class bool 11.43: undeclared member f in class int 11.42: not-expression requires boolean operand 11.42: incorrect type of + RHS (expected int, found bool) 13.5: type mismatch in assignment, lhs=int rhs=D 14.5: undeclared member o in class C 14.5: undeclared member f in class int 15.6: undeclared member a in class C 15.10: undeclared member b in class C 15.5: undeclared member y in class int 15.18: undefined class or channel T used in new expression 16.19: undeclared member O in class C 16.14: == requires operands of the same type, found int and bool 16.31: undeclared member O in class C 16.13: != requires operands of the same type, found bool and int 16.13: object in reorder statement must be of a reference type (found bool) 16.41: undeclared member a in class C 16.41: install bound must be of a reference type or Mu type (found int) 16.43: undeclared member b in class C 16.43: install bound must be of a reference type or Mu type (found int) 16.45: undeclared member c in class C 16.45: install bound must be of a reference type or Mu type (found int) 16.51: install bound must be of a reference type or Mu type (found int) 16.53: install bound must be of a reference type or Mu type (found int) 17.13: undeclared member X in class C 17.19: undeclared member Y in class C 17.13: incorrect type of ==> LHS (expected bool, found int) 17.19: incorrect type of ==> RHS (expected bool, found int) 17.13: object in reorder statement must be of a reference type (found bool) 17.27: install bound must be of a reference type or Mu type (found int) 18.13: undeclared member o in class C 18.13: undeclared member f in class int 18.13: object in reorder statement must be of a reference type (found int) 19.11: undeclared member o in class C 19.11: object in share statement must be of a reference type (found int) 20.13: undeclared member o in class C 20.13: object in unshare statement must be of a reference type (found int) 21.13: undeclared member o in class C 21.13: object in acquire statement must be of a reference type (found int) 22.13: undeclared member o in class C 22.13: object in release statement must be of a reference type (found int) 23.16: undeclared member o in class C 23.16: object in rd acquire statement must be of a reference type (found int) 24.16: undeclared member o in class C 24.16: object in rd release statement must be of a reference type (found int) 25.15: undeclared member o in class C 25.15: object in downgrade statement must be of a reference type (found int) 27.17: undeclared member o in class C 27.5: call of undeclared member m in class int 27.10: wrong token type 29.12: rd expression is allowed only in positive predicate contexts 29.15: undeclared member x in class C 29.20: acc expression is allowed only in positive predicate contexts 29.24: undeclared member y in class C 29.12: incorrect type of + LHS (expected int, found bool) 29.20: incorrect type of + RHS (expected int, found bool) 29.29: acc expression is allowed only in positive predicate contexts 29.33: undeclared member z in class C 29.29: incorrect type of + RHS (expected int, found bool) 29.51: undeclared member k in class C 29.57: undeclared member f in class null 29.12: assert statement requires a boolean expression (found int) 30.10: undeclared member f in class C 31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0) 32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0) 33.19: undeclared member o in class C 33.10: undefined local variable a 33.12: undefined local variable b 33.14: undefined local variable c 33.5: call of undeclared member m in class int 34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0) 34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0) 35.13: undeclared member o in class C 35.13: object in reorder statement must be of a reference type (found int) 58.17: undeclared member sqrt2 in class C 58.25: undeclared member sqrt2 in class C 62.17: undeclared member s in class C 62.10: undefined local variable v 62.5: call of undeclared member M in class int ------ Running regression test prog1.chalice 9.10: Location might not be readable. 25.5: Location might not be writable 33.14: Location might not be readable. 42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true. 60.5: Location might not be writable 76.5: The held field of the target of the unshare statement might not be writable. 84.5: The held field of the target of the unshare statement might not be writable. Boogie program verifier finished with 16 verified, 7 errors ------ Running regression test prog2.chalice 24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true. 31.13: Location might not be readable. 73.5: Const variable can be assigned to only once. 78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true. Boogie program verifier finished with 24 verified, 4 errors ------ Running regression test prog3.chalice 76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true. 76.3: Method might lock/unlock more than allowed. 191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x. 202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x. Boogie program verifier finished with 51 verified, 4 errors ------ Running regression test prog4.chalice 5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true. 15.7: The held field of the target of the release statement might not be writable. 27.7: The held field of the target of the release statement might not be writable. Boogie program verifier finished with 6 verified, 3 errors ------ Running regression test RockBand.chalice 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid. 41.10: Location might not be readable. 50.5: Location might not be writable 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid. 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid. 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid. Boogie program verifier finished with 29 verified, 6 errors ------ Running regression test swap.chalice Boogie program verifier finished with 5 verified, 0 errors ------ Running regression test GhostConst.chalice The program did not typecheck. 7.27: undeclared member c in class C 13.10: ghost variable not allowed here 21.10: ghost variable not allowed here 29.10: ghost fields not allowed here ------ Running regression test OwickiGries.chalice Boogie program verifier finished with 5 verified, 0 errors ------ Running regression test ProdConsChannel.chalice 47.3: Method body is not allowed to leave any debt. 61.3: Method body is not allowed to leave any debt. 85.20: Location might not be readable. 123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true. Boogie program verifier finished with 19 verified, 4 errors ------ Running regression test cell-defaults.chalice 96.5: The heap of the callee might not be strictly smaller than the heap of the caller. 102.5: The heap of the callee might not be strictly smaller than the heap of the caller. 131.5: Assertion might not hold. Automatic fold might fail. Insufficient fraction at 42.5 for Cell.x. Boogie program verifier finished with 29 verified, 3 errors ------ Running regression test RockBand-automagic.chalice Boogie program verifier finished with 35 verified, 0 errors ------ Running regression test Leaks.chalice 6.3: Monitor invariant is not allowed to hold write permission to this.mu 11.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<