Merge

2 files changed, 39 insertions, 29 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4feaf762..3bee3088 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2087,14 +2087,14 @@ SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decrease
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(669,14): Error: assertion violation

+SmallTests.dfy(679,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(666,5): anon7_LoopHead

+    SmallTests.dfy(676,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(666,5): anon8_Else

+    SmallTests.dfy(676,5): anon8_Else

     (0,0): anon9_Then

-SmallTests.dfy(690,14): Error: assertion violation

+SmallTests.dfy(700,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

@@ -2127,12 +2127,12 @@ SmallTests.dfy(390,41): Related location: This is the postcondition that might n
 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-SmallTests.dfy(540,12): Error: assertion violation

+SmallTests.dfy(550,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-SmallTests.dfy(554,20): Error: left-hand sides 0 and 1 may refer to the same location

+SmallTests.dfy(564,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -2144,11 +2144,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-SmallTests.dfy(556,15): Error: left-hand sides 1 and 2 may refer to the same location

+SmallTests.dfy(566,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(549,18): anon28_Else

+    SmallTests.dfy(559,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -2160,16 +2160,16 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(563,25): Error: target object may be null

+SmallTests.dfy(573,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(576,10): Error: assertion violation

+SmallTests.dfy(586,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(600,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(610,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(623,10): Error: assertion violation

+SmallTests.dfy(633,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -2177,21 +2177,21 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-SmallTests.dfy(637,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(647,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(639,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(649,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(652,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(662,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 85 verified, 33 errors

+Dafny program verifier finished with 87 verified, 33 errors

 out.tmp.dfy(33,11): Error: index out of range

 Execution trace:

     (0,0): anon0

@@ -2313,12 +2313,12 @@ out.tmp.dfy(499,41): Related location: This is the postcondition that might not
 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-out.tmp.dfy(536,12): Error: assertion violation

+out.tmp.dfy(544,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-out.tmp.dfy(550,20): Error: left-hand sides 0 and 1 may refer to the same location

+out.tmp.dfy(558,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -2330,11 +2330,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-out.tmp.dfy(552,15): Error: left-hand sides 1 and 2 may refer to the same location

+out.tmp.dfy(560,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    out.tmp.dfy(545,17): anon28_Else

+    out.tmp.dfy(553,17): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -2346,16 +2346,16 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(559,25): Error: target object may be null

+out.tmp.dfy(567,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(572,10): Error: assertion violation

+out.tmp.dfy(580,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(598,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(606,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(617,10): Error: assertion violation

+out.tmp.dfy(625,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -2363,21 +2363,21 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-out.tmp.dfy(631,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(639,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

-out.tmp.dfy(633,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(641,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-out.tmp.dfy(647,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(655,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 85 verified, 33 errors

+Dafny program verifier finished with 87 verified, 33 errors

 

 -------------------- LetExpr.dfy --------------------

 LetExpr.dfy(5,12): Error: assertion violation

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 75a42200..b3107bcb 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -190,7 +190,7 @@ class AllocatedTests {
   {

     var n := new Node;

     var t := S + {n};

-    

+

     if (*) {

       assert !fresh(n);  // error: n was not allocated in the initial state

     } else {

@@ -498,6 +498,16 @@ class AttributeTests {
   }

 }

 

+// ----------------------- test attributes on variable declarations --------

+

+static method TestAttributesVarDecls()

+{

+  var {:foo} foo;

+  var {:bar} bar := 0;

+  var {:foo} {:bar} foobar := {};

+  var {:baz} baz, {:foobaz} foobaz := true, false;

+}

+

 // ----------------------- Pretty printing of !(!expr) --------

 

 static method TestNotNot()