Allocated 4 default (#3637)

This PR makes `/allocated:4` the default, which addresses soundness issues with `/allocated:3`. The PR also deprecates the `/allocated` option. Going forward, Dafny will support only one encoding of the allocation state (namely, the one that's `/allocated:4`). As far as I know, the previous users of `/allocated:1` or `/allocated:2` are no longer using an `/allocated` setting. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · Feb 28, 2023 · 4e9425b · 4e9425b
1 parent a424583
commit 4e9425b
Show file tree

Hide file tree

Showing 108 changed files with 122 additions and 5 deletions.
diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
@@ -314,7 +314,7 @@ public enum IncludesModes {
     public int OptimizeResolution = 2;
     public bool UseRuntimeLib = false;
     public bool DisableScopes = false;
-    public int Allocated = 3;
+    public int Allocated = 4;
     public bool UseStdin = false;
     public bool WarningsAsErrors = false;
     [CanBeNull] private TestGenerationOptions testGenOptions = null;
@@ -685,6 +685,9 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
 
         case "allocated": {
             ps.GetIntArgument(ref Allocated, 5);
+            if (Allocated != 4) {
+              Printer.AdvisoryWriteLine(Console.Out, "The /allocated:<n> option is deprecated");
+            }
             return true;
           }
 
@@ -1395,6 +1398,8 @@ quantifiers and lemmas.
        print effects only if it is marked with {{:print}}.
 
 /allocated:<n>
+    This option is deprecated. Going forward, only what is /allocated:4
+    will be supported.
     Specify defaults for where Dafny should assert and assume
     allocated(x) for various parameters x, local variables x, bound
     variables x, etc. Lower <n> may require more manual allocated(x)
@@ -1413,8 +1418,8 @@ not sound in general.
     2 - Assert/assume allocated(x) on all variables, even bound
         variables in quantifiers. This option is the easiest to use for
         heapful code.
-    3 - (default) Frugal use of heap parameters.
-    4 - Mode 3 but with alloc antecedents when ranges don't imply
+    3 - Frugal use of heap parameter (not sound).
+    4 - (default) Mode 3 but with alloc antecedents when ranges don't imply
         allocatedness.
 
 /definiteAssignment:<n>

diff --git a/Test/allocated1/Allocated1.dfy.expect b/Test/allocated1/Allocated1.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 AllocatedCommon.dfyi(23,26): Error: assertion might not hold
 AllocatedCommon.dfyi(24,26): Error: assertion might not hold
 AllocatedCommon.dfyi(25,26): Error: assertion might not hold

diff --git a/Test/allocated1/Allocated2.dfy.expect b/Test/allocated1/Allocated2.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Allocated2.dfy(4,8): Error: the included file AllocatedCommon.dfyi contains error(s)
 AllocatedCommon.dfyi(23,26): Error: a function definition is not allowed to depend on the set of allocated references
 AllocatedCommon.dfyi(24,26): Error: a function definition is not allowed to depend on the set of allocated references

diff --git a/Test/allocated1/dafny0/AdvancedLHS.dfy.expect b/Test/allocated1/dafny0/AdvancedLHS.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 AdvancedLHS.dfy(34,22): Error: target object might be null
 
 Dafny program verifier finished with 3 verified, 1 error
diff --git a/Test/allocated1/dafny0/AllLiteralsAxiom.dfy.expect b/Test/allocated1/dafny0/AllLiteralsAxiom.dfy.expect
@@ -1,2 +1,3 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/allocated1/dafny0/Array.dfy.expect b/Test/allocated1/dafny0/Array.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Array.dfy(13,7): Error: assignment might update an array element not in the enclosing context's modifies clause
 Array.dfy(20,15): Error: target object might be null
 Array.dfy(26,5): Error: index out of range

diff --git a/Test/allocated1/dafny0/AssertBy.dfy.expect b/Test/allocated1/dafny0/AssertBy.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 // AssertBy.dfy
 
 method M0(x: int, y: int)

diff --git a/Test/allocated1/dafny0/AssumptionVariables1.dfy.expect b/Test/allocated1/dafny0/AssumptionVariables1.dfy.expect
@@ -1,2 +1,3 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/allocated1/dafny0/AutoContracts.dfy.expect b/Test/allocated1/dafny0/AutoContracts.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 AutoContracts.dfy(17,4): Error: A postcondition might not hold on this return path.
 AutoContracts.dfy(17,4): Related location: This is the postcondition that might not hold.
 AutoContracts.dfy(12,20): Related location

diff --git a/Test/allocated1/dafny0/AutoReq.dfy.expect b/Test/allocated1/dafny0/AutoReq.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 AutoReq.dfy(247,4): Error: function precondition might not hold
 AutoReq.dfy(239,13): Related location
 AutoReq.dfy(239,35): Related location

diff --git a/Test/allocated1/dafny0/Backticks.dfy.expect b/Test/allocated1/dafny0/Backticks.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Backticks.dfy(38,4): Error: insufficient reads clause to invoke function
 Backticks.dfy(77,7): Error: call might violate context's modifies clause
 

diff --git a/Test/allocated1/dafny0/BadFunction.dfy.expect b/Test/allocated1/dafny0/BadFunction.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 BadFunction.dfy(9,2): Error: decreases clause might not decrease
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/Test/allocated1/dafny0/Basics.dfy.expect b/Test/allocated1/dafny0/Basics.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Basics.dfy(623,17): Error: result of operation might violate newtype constraint for 'int8'
 Basics.dfy(45,13): Error: assertion might not hold
 Basics.dfy(69,41): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/BindingGuards.dfy.expect b/Test/allocated1/dafny0/BindingGuards.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 BindingGuards.dfy(85,10): Error: A postcondition might not hold on this return path.
 BindingGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
 BindingGuards.dfy(134,9): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/Bitvectors.dfy.expect b/Test/allocated1/dafny0/Bitvectors.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 11 verified, 0 errors
 4000 4000 4000 0

diff --git a/Test/allocated1/dafny0/BitvectorsMore.dfy.expect b/Test/allocated1/dafny0/BitvectorsMore.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 BitvectorsMore.dfy(13,9): Error: possible division by zero
 BitvectorsMore.dfy(17,13): Error: possible division by zero
 BitvectorsMore.dfy(21,13): Error: possible division by zero

diff --git a/Test/allocated1/dafny0/Calculations.dfy.expect b/Test/allocated1/dafny0/Calculations.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Calculations.dfy(7,5): Error: index out of range
 Calculations.dfy(12,14): Error: index out of range
 Calculations.dfy(12,18): Error: assertion might not hold
@@ -6,5 +7,6 @@ Calculations.dfy(79,14): Error: index out of range
 Calculations.dfy(79,18): Error: assertion might not hold
 
 Dafny program verifier finished with 3 verified, 6 errors
+The /allocated:<n> option is deprecated
 
 Dafny program verifier did not attempt verification
diff --git a/Test/allocated1/dafny0/ChainingDisjointTests.dfy.expect b/Test/allocated1/dafny0/ChainingDisjointTests.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ChainingDisjointTests.dfy(49,2): Error: A postcondition might not hold on this return path.
 ChainingDisjointTests.dfy(48,14): Related location: This is the postcondition that might not hold.
 ChainingDisjointTests.dfy(42,22): Related location

diff --git a/Test/allocated1/dafny0/Char.dfy.expect b/Test/allocated1/dafny0/Char.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Char.dfy(81,13): Error: char addition might overflow
 Char.dfy(89,7): Error: char subtraction might underflow
 Char.dfy(48,20): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/CoPrefix.dfy.expect b/Test/allocated1/dafny0/CoPrefix.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 CoPrefix.dfy(164,2): Error: A postcondition might not hold on this return path.
 CoPrefix.dfy(163,14): Related location: This is the postcondition that might not hold.
 CoPrefix.dfy(169,2): Error: A postcondition might not hold on this return path.

diff --git a/Test/allocated1/dafny0/CoinductiveProofs.dfy.expect b/Test/allocated1/dafny0/CoinductiveProofs.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 CoinductiveProofs.dfy(30,11): Error: assertion might not hold
 CoinductiveProofs.dfy(15,42): Related location
 CoinductiveProofs.dfy(13,16): Related location

diff --git a/Test/allocated1/dafny0/Compilation.dfy.expect b/Test/allocated1/dafny0/Compilation.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 29 verified, 0 errors
 400

diff --git a/Test/allocated1/dafny0/CompilationErrors.dfy.expect b/Test/allocated1/dafny0/CompilationErrors.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 CompilationErrors.dfy(71,2): Warning: note, this loop has no body (loop frame: x)
 CompilationErrors.dfy(73,2): Warning: note, this loop has no body (loop frame: i, x)
 CompilationErrors.dfy(83,4): Warning: note, this loop has no body (loop frame: x)

diff --git a/Test/allocated1/dafny0/Comprehensions.dfy.expect b/Test/allocated1/dafny0/Comprehensions.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Comprehensions.dfy(6,17): Warning: /!\ No terms found to trigger on.
 Comprehensions.dfy(22,11): Warning: /!\ No terms found to trigger on.
 Comprehensions.dfy(24,7): Warning: /!\ No terms found to trigger on.

diff --git a/Test/allocated1/dafny0/Computations.dfy.expect b/Test/allocated1/dafny0/Computations.dfy.expect
@@ -1,2 +1,3 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 44 verified, 0 errors
diff --git a/Test/allocated1/dafny0/ComputationsLoop.dfy.expect b/Test/allocated1/dafny0/ComputationsLoop.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ComputationsLoop.dfy(7,2): Error: decreases clause might not decrease
 ComputationsLoop.dfy(12,25): Error: assertion might not hold
 

diff --git a/Test/allocated1/dafny0/ComputationsLoop2.dfy.expect b/Test/allocated1/dafny0/ComputationsLoop2.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ComputationsLoop2.dfy(6,2): Error: cannot prove termination; try supplying a decreases clause
 ComputationsLoop2.dfy(11,2): Error: cannot prove termination; try supplying a decreases clause
 ComputationsLoop2.dfy(16,25): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/ComputationsNeg.dfy.expect b/Test/allocated1/dafny0/ComputationsNeg.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ComputationsNeg.dfy(7,2): Error: decreases clause might not decrease
 ComputationsNeg.dfy(11,0): Error: A postcondition might not hold on this return path.
 ComputationsNeg.dfy(10,16): Related location: This is the postcondition that might not hold.

diff --git a/Test/allocated1/dafny0/ContainerRanks.dfy.expect b/Test/allocated1/dafny0/ContainerRanks.dfy.expect
@@ -1,2 +1,3 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/allocated1/dafny0/ControlStructures.dfy.expect b/Test/allocated1/dafny0/ControlStructures.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ControlStructures.dfy(8,2): Error: missing case in match statement: Purple
 ControlStructures.dfy(8,2): Error: missing case in match statement: Blue
 ControlStructures.dfy(17,2): Error: missing case in match statement: Purple

diff --git a/Test/allocated1/dafny0/Corecursion.dfy.expect b/Test/allocated1/dafny0/Corecursion.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Corecursion.dfy(17,12): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
 Corecursion.dfy(23,12): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)
 Corecursion.dfy(58,4): Error: cannot prove termination; try supplying a decreases clause

diff --git a/Test/allocated1/dafny0/DTypes.dfy.expect b/Test/allocated1/dafny0/DTypes.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 DTypes.dfy(214,14): Warning: the type of the other operand is a non-null type, so this comparison with 'null' will always return 'false' (to make it possible for variable 'm' to have the value 'null', declare its type to be 'MyClass?')
 DTypes.dfy(215,14): Warning: the type of the other operand is a non-null type, so this comparison with 'null' will always return 'false' (to make it possible for variable 'b' to have the value 'null', declare its type to be 'Cell?<MyClass>')
 DTypes.dfy(222,14): Warning: the type of the other operand is a non-null type, so this comparison with 'null' will always return 'false' (to make it possible for variable 'm' to have the value 'null', declare its type to be 'MyClass?')

diff --git a/Test/allocated1/dafny0/DatatypeUpdate.dfy.expect b/Test/allocated1/dafny0/DatatypeUpdate.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 DatatypeUpdate.dfy(67,15): Error: destructor 'b' can only be applied to datatype values constructed by 'BB'
 DatatypeUpdate.dfy(69,15): Error: source of datatype update must be constructed by 'BB'
 

diff --git a/Test/allocated1/dafny0/Datatypes.dfy.expect b/Test/allocated1/dafny0/Datatypes.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Datatypes.dfy(297,9): Error: A postcondition might not hold on this return path.
 Datatypes.dfy(295,14): Related location: This is the postcondition that might not hold.
 Datatypes.dfy(298,11): Error: missing case in match expression: Appendix(_)

diff --git a/Test/allocated1/dafny0/Definedness.dfy.expect b/Test/allocated1/dafny0/Definedness.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Definedness.dfy(11,6): Error: possible division by zero
 Definedness.dfy(18,15): Error: possible division by zero
 Definedness.dfy(27,15): Error: target object might be null

diff --git a/Test/allocated1/dafny0/DeterministicPick.dfy.expect b/Test/allocated1/dafny0/DeterministicPick.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 DeterministicPick.dfy(13,4): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
 
 Dafny program verifier finished with 5 verified, 1 error
diff --git a/Test/allocated1/dafny0/DiamondImports.dfy.expect b/Test/allocated1/dafny0/DiamondImports.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 DiamondImports.dfy(34,15): Error: assertion might not hold
 DiamondImports.dfy(50,15): Error: assertion might not hold
 DiamondImports.dfy(101,15): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/DirtyLoops.dfy.expect b/Test/allocated1/dafny0/DirtyLoops.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 DirtyLoops.dfy(26,2): Warning: note, this loop has no body (loop frame: i)
 DirtyLoops.dfy(35,2): Warning: note, this loop has no body (loop frame: i)
 DirtyLoops.dfy(46,2): Warning: note, this loop has no body (loop frame: i)
@@ -92,6 +93,7 @@ DirtyLoops.dfy(468,6): Error: loop modifies clause might violate context's modif
 DirtyLoops.dfy(485,6): Error: loop modifies clause might violate context's modifies clause
 
 Dafny program verifier finished with 22 verified, 46 errors
+The /allocated:<n> option is deprecated
 DirtyLoops.dfy.tmp.dprint.dfy(446,4): Warning: note, this loop has no body (loop frame: $Heap)
 DirtyLoops.dfy.tmp.dprint.dfy(455,4): Warning: note, this loop has no body (loop frame: $Heap)
 DirtyLoops.dfy.tmp.dprint.dfy(471,6): Warning: note, this loop has no body (loop frame: i, $Heap)

diff --git a/Test/allocated1/dafny0/DiscoverBounds.dfy.expect b/Test/allocated1/dafny0/DiscoverBounds.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 DiscoverBounds.dfy(32,7): Warning: /!\ No terms found to trigger on.
 DiscoverBounds.dfy(33,7): Warning: /!\ No terms found to trigger on.
 DiscoverBounds.dfy(34,7): Warning: /!\ No terms found to trigger on.

diff --git a/Test/allocated1/dafny0/ForallCompilation.dfy.expect b/Test/allocated1/dafny0/ForallCompilation.dfy.expect
@@ -1,2 +1,3 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Test/allocated1/dafny0/Fuel.dfy.expect b/Test/allocated1/dafny0/Fuel.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Fuel.dfy(3,8): Error: the included file Fuel.dfy contains error(s)
 Fuel.dfy(129,8): Error: Fuel can only increase within a given scope.
 Fuel.dfy(407,8): Error: Fuel can only increase within a given scope.

diff --git a/Test/allocated1/dafny0/FunctionSpecifications.dfy.expect b/Test/allocated1/dafny0/FunctionSpecifications.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 FunctionSpecifications.dfy(35,24): Error: A postcondition might not hold on this return path.
 FunctionSpecifications.dfy(31,12): Related location: This is the postcondition that might not hold.
 FunctionSpecifications.dfy(45,2): Error: A postcondition might not hold on this return path.

diff --git a/Test/allocated1/dafny0/IMaps.dfy.expect b/Test/allocated1/dafny0/IMaps.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 IMaps.dfy(36,18): Warning: /!\ No terms found to trigger on.
 IMaps.dfy(36,49): Warning: /!\ No terms found to trigger on.
 IMaps.dfy(51,18): Warning: /!\ No terms found to trigger on.

diff --git a/Test/allocated1/dafny0/ISets.dfy.expect b/Test/allocated1/dafny0/ISets.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ISets.dfy(38,15): Warning: /!\ No terms found to trigger on.
 ISets.dfy(40,9): Warning: /!\ No terms found to trigger on.
 

diff --git a/Test/allocated1/dafny0/InSetComprehension.dfy.expect b/Test/allocated1/dafny0/InSetComprehension.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 InSetComprehension.dfy(10,17): Warning: /!\ No terms found to trigger on.
 InSetComprehension.dfy(12,17): Warning: /!\ No terms found to trigger on.
 InSetComprehension.dfy(14,16): Info: Selected triggers: {Even(m)}

diff --git a/Test/allocated1/dafny0/IndexIntoUpdate.dfy.expect b/Test/allocated1/dafny0/IndexIntoUpdate.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 IndexIntoUpdate.dfy(7,18): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/Test/allocated1/dafny0/InductivePredicates.dfy.expect b/Test/allocated1/dafny0/InductivePredicates.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 InductivePredicates.dfy(80,9): Error: assertion might not hold
 InductivePredicates.dfy(92,10): Error: assertion might not hold
 

diff --git a/Test/allocated1/dafny0/Inverses.dfy.expect b/Test/allocated1/dafny0/Inverses.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Inverses.dfy(70,2): Error: A postcondition might not hold on this return path.
 Inverses.dfy(67,10): Related location: This is the postcondition that might not hold.
 Inverses.dfy(67,40): Related location

diff --git a/Test/allocated1/dafny0/JustWarnings.dfy.expect b/Test/allocated1/dafny0/JustWarnings.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 JustWarnings.dfy(18,11): Warning: Shadowed type-parameter name: T
 JustWarnings.dfy(13,6): Warning: Shadowed local-variable name: x
 

diff --git a/Test/allocated1/dafny0/LetExpr.dfy.expect b/Test/allocated1/dafny0/LetExpr.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 LetExpr.dfy(45,2): Warning: /!\ No terms found to trigger on.
 LetExpr.dfy(206,4): Warning: /!\ No terms found to trigger on.
 LetExpr.dfy(340,18): Error: value does not satisfy the subset constraints of 'nat'
@@ -15,6 +16,7 @@ LetExpr.dfy(323,11): Error: to be compilable, the value of a let-such-that expre
 LetExpr.dfy(109,22): Error: assertion might not hold
 
 Dafny program verifier finished with 37 verified, 13 errors
+The /allocated:<n> option is deprecated
 LetExpr.dfy.tmp.dprint.dfy(281,4): Warning: /!\ No terms found to trigger on.
 LetExpr.dfy.tmp.dprint.dfy(46,2): Warning: /!\ No terms found to trigger on.
 

diff --git a/Test/allocated1/dafny0/LhsDuplicates.dfy.expect b/Test/allocated1/dafny0/LhsDuplicates.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 LhsDuplicates.dfy(21,9): Error: left-hand sides for different forall-statement bound variables might refer to the same location
 LhsDuplicates.dfy(36,11): Error: left-hand sides for different forall-statement bound variables might refer to the same location
 LhsDuplicates.dfy(42,5): Error: left-hand sides a and a refer to the same location

diff --git a/Test/allocated1/dafny0/LitTriggers.dfy.expect b/Test/allocated1/dafny0/LitTriggers.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 LitTriggers.dfy(56,21): Error: assertion might not hold
 
 Dafny program verifier finished with 5 verified, 1 error
diff --git a/Test/allocated1/dafny0/LoopModifies.dfy.expect b/Test/allocated1/dafny0/LoopModifies.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 LoopModifies.dfy(8,4): Error: assignment might update an array element not in the enclosing context's modifies clause
 LoopModifies.dfy(19,7): Error: assignment might update an array element not in the enclosing context's modifies clause
 LoopModifies.dfy(48,7): Error: assignment might update an array element not in the enclosing context's modifies clause

diff --git a/Test/allocated1/dafny0/Maps.dfy.expect b/Test/allocated1/dafny0/Maps.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Maps.dfy(200,11): Warning: /!\ No terms found to trigger on.
 Maps.dfy(78,7): Error: element might not be in domain
 Maps.dfy(128,17): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/MatchBraces.dfy.expect b/Test/allocated1/dafny0/MatchBraces.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 // MatchBraces.dfy
 
 method Main()

diff --git a/Test/allocated1/dafny0/Matrix-OOB.dfy.expect b/Test/allocated1/dafny0/Matrix-OOB.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Matrix-OOB.dfy(11,10): Info: Selected triggers: {m[i, j]}
 Matrix-OOB.dfy(11,27): Error: index 0 out of range
 Matrix-OOB.dfy(11,30): Error: index 1 out of range

diff --git a/Test/allocated1/dafny0/ModifyStmt.dfy.expect b/Test/allocated1/dafny0/ModifyStmt.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 ModifyStmt.dfy(135,4): Warning: the modify statement with a block statement is deprecated
 ModifyStmt.dfy(143,4): Warning: the modify statement with a block statement is deprecated
 ModifyStmt.dfy(150,4): Warning: the modify statement with a block statement is deprecated

diff --git a/Test/allocated1/dafny0/Modules1.dfy.expect b/Test/allocated1/dafny0/Modules1.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Modules1.dfy(10,8): Error: target object might not be allocated
 Modules1.dfy(82,15): Error: assertion might not hold
 Modules1.dfy(95,15): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/MultiDimArray.dfy.expect b/Test/allocated1/dafny0/MultiDimArray.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 MultiDimArray.dfy(53,20): Error: assertion might not hold
 MultiDimArray.dfy(79,24): Error: assertion might not hold
 

diff --git a/Test/allocated1/dafny0/MultiSets.dfy.expect b/Test/allocated1/dafny0/MultiSets.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 MultiSets.dfy(177,19): Error: new number of occurrences might be negative
 MultiSets.dfy(268,23): Error: assertion might not hold
 MultiSets.dfy(291,15): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/NatTypes.dfy.expect b/Test/allocated1/dafny0/NatTypes.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 NatTypes.dfy(10,4): Error: value does not satisfy the subset constraints of 'nat'
 NatTypes.dfy(44,31): Error: value does not satisfy the subset constraints of 'nat'
 NatTypes.dfy(51,15): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/NestedMatch.dfy.expect b/Test/allocated1/dafny0/NestedMatch.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 NestedMatch.dfy(173,14): Error: the calculation step between the previous line and this line might not hold
 
 Dafny program verifier finished with 12 verified, 1 error
diff --git a/Test/allocated1/dafny0/Newtypes.dfy.expect b/Test/allocated1/dafny0/Newtypes.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Newtypes.dfy(74,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
 Newtypes.dfy(76,44): Error: possible division by zero
 Newtypes.dfy(87,13): Error: result of operation might violate newtype constraint for 'char8'

diff --git a/Test/allocated1/dafny0/NoTypeArgs.dfy.expect b/Test/allocated1/dafny0/NoTypeArgs.dfy.expect
@@ -1,2 +1,3 @@
+The /allocated:<n> option is deprecated
 
 Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/allocated1/dafny0/OpaqueFunctions.dfy.expect b/Test/allocated1/dafny0/OpaqueFunctions.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 OpaqueFunctions.dfy(38,15): Error: assertion might not hold
 OpaqueFunctions.dfy(69,7): Error: A precondition for this call might not hold.
 OpaqueFunctions.dfy(35,15): Related location: This is the precondition that might not hold.

diff --git a/Test/allocated1/dafny0/Parallel.dfy.expect b/Test/allocated1/dafny0/Parallel.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Parallel.dfy(267,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
 Parallel.dfy(279,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
 Parallel.dfy(286,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead

diff --git a/Test/allocated1/dafny0/PredExpr.dfy.expect b/Test/allocated1/dafny0/PredExpr.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 PredExpr.dfy(7,11): Error: assertion might not hold
 PredExpr.dfy(39,14): Error: value does not satisfy the subset constraints of 'nat'
 PredExpr.dfy(52,16): Error: assertion might not hold

diff --git a/Test/allocated1/dafny0/Predicates.dfy.expect b/Test/allocated1/dafny0/Predicates.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Predicates.dfy(62,15): Error: assertion might not hold
 Predicates.dfy(66,13): Error: assertion might not hold
 Predicates.dfy(94,31): Error: target object might not be allocated

diff --git a/Test/allocated1/dafny0/Protected.dfy.expect b/Test/allocated1/dafny0/Protected.dfy.expect
@@ -1,3 +1,4 @@
+The /allocated:<n> option is deprecated
 Protected.dfy(21,19): Error: assertion might not hold
 Protected.dfy(35,17): Error: assertion might not hold
 Protected.dfy(39,15): Error: assertion might not hold
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,3 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 4 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,3 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 2 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,3 +1,4 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 29 verified, 0 errors
		400
Expand Down
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,3 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 44 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,3 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 5 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,3 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 14 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,3 @@
		The /allocated:<n> option is deprecated

		Dafny program verifier finished with 7 verified, 0 errors