Initial set of files.

1 files changed, 235 insertions, 0 deletions

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
new file mode 100644
index 00000000..b81e3893
--- /dev/null
+++ b/Chalice/examples/Answer
@@ -0,0 +1,235 @@
+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

+<undefined position>: not-expression requires boolean operand

+<undefined position>: 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 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 install 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 install 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 install 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 install 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 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<<o.mu

+  16.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

+  29.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu

+  62.3: Monitor invariant is not allowed to hold write permission to this.mu

+

+Boogie program verifier finished with 7 verified, 5 errors