Marked "free" as soon-to-be-deprecated

4 files changed, 39 insertions, 31 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2134ba6d..84f09ee0 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -777,7 +777,9 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
                  { "," FrameExpression<out fe>               (. mod.Add(fe); .)

                  }

                ] OldSemi

-  | [ "free"                                                 (. isFree = true; .)

+  | [ "free"                                                 (. isFree = true;

+                                                                errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+                                                             .)

     ]

     ( "requires" Expression<out e, false, true> OldSemi      (. req.Add(new MaybeFreeExpression(e, isFree)); .)

     | "ensures"

@@ -804,7 +806,9 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
                  { "," FrameExpression<out fe>               (. mod.Add(fe); .)

                  }

                ] OldSemi

-  | [ "free"                                                 (. isFree = true; .)

+  | [ "free"                                                 (. isFree = true;

+                                                                errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+                                                             .)

     ]

     [ "yield"                                                (. isYield = true; .)

     ]

@@ -1463,7 +1467,9 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
 Invariant<out MaybeFreeExpression/*!*/ invariant>

 = (. bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; .)

     SYNC

-    ["free"                            (. isFree = true; .)

+    ["free"                            (. isFree = true;

+                                          errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+                                       .)

     ]

     "invariant" { IF(IsAttribute()) Attribute<ref attrs> }

     Expression<out e, false, true>           (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)

@@ -1609,7 +1615,9 @@ ForallStmt<out Statement/*!*/ s>
   |                                         (. if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } .)

   )

   {                                         (. isFree = false; .)

-    [ "free"                                (. isFree = true; .)

+    [ "free"                                (. isFree = true;

+                                               errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+                                            .)

     ]

     "ensures" Expression<out e, false, true>  (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

     OldSemi                                   (. tok = t; .)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 20f9332d..2358fc79 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1465,7 +1465,9 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 		} else if (StartOf(14)) {

 			if (la.kind == 54) {

 				Get();

-				isFree = true; 

+				isFree = true;

+				errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+				

 			}

 			if (la.kind == 57) {

 				Get();

@@ -1543,7 +1545,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 14 || la.kind == 54 || la.kind == 55) {

 			if (la.kind == 54) {

 				Get();

-				isFree = true; 

+				isFree = true;

+				errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+				

 			}

 			if (la.kind == 14) {

 				Get();

@@ -2226,7 +2230,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			isFree = false; 

 			if (la.kind == 54) {

 				Get();

-				isFree = true; 

+				isFree = true;

+				errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+				

 			}

 			Expect(55);

 			Expression(out e, false, true);

@@ -2582,7 +2588,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (!(la.kind == 0 || la.kind == 54 || la.kind == 88)) {SynErr(195); Get();}

 		if (la.kind == 54) {

 			Get();

-			isFree = true; 

+			isFree = true;

+			errors.Warning(t, "the 'free' keyword is soon to be deprecated");

+			

 		}

 		Expect(88);

 		while (IsAttribute()) {

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index d6658671..0482e4ec 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -432,10 +432,6 @@ class AttributeTests {
     ensures {:boolAttr false} true;

     ensures {:intAttr 0} true;

     ensures {:intAttr 1} true;

-    free ensures {:boolAttr true} true;

-    free ensures {:boolAttr false} true;

-    free ensures {:intAttr 0} true;

-    free ensures {:intAttr 1} true;

     modifies {:boolAttr true} this`f;

     modifies {:boolAttr false} this`f;

     modifies {:intAttr 0} this`f;

@@ -459,10 +455,6 @@ class AttributeTests {
       invariant {:boolAttr false} true;

       invariant {:intAttr 0} true;

       invariant {:intAttr 1} true;

-      free invariant {:boolAttr true} true;

-      free invariant {:boolAttr false} true;

-      free invariant {:intAttr 0} true;

-      free invariant {:intAttr 1} true;

       modifies {:boolAttr true} this`f;

       modifies {:boolAttr false} this`f;

       modifies {:intAttr 0} this`f;

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 1e71ec8b..87cc4a84 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -94,14 +94,14 @@ SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decrease
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

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

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

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(686,5): anon7_LoopHead

+    SmallTests.dfy(678,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(686,5): anon8_Else

+    SmallTests.dfy(678,5): anon8_Else

     (0,0): anon9_Then

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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

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

     (0,0): anon0

     (0,0): anon6_Else

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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

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

     (0,0): anon32_Then

     (0,0): anon12

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

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

+    SmallTests.dfy(561,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon30_Then

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

     (0,0): anon22

     (0,0): anon38_Then

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -182,17 +182,17 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-SmallTests.dfy(657,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_Then

     (0,0): anon6_Then

     (0,0): anon3

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

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

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

 Execution trace:

     (0,0): anon0