Enable Boogie variables to be monotonic

Source/Core/AST/Absy.cs

@@ -1304,6 +1304,15 @@ public Variable(IToken tok, TypedIdent typedIdent, QKeyValue kv)
     }
 
     public abstract bool IsMutable { get; }
+
+    /// <summary>
+    /// Prevents this variable from being havoc'd. Useful in situations where Havoc commands are generated,
+    /// such as after While commands.
+    ///
+    /// One use-case is the definite assignment tracking variables in Dafny, that only go from false to true,
+    /// And can return an error if they're still false at the wrong point.
+    /// </summary>
+    public bool Monotonic { get; set;  }
 
     public override void Emit(TokenTextWriter stream, int level)
     {

Source/Core/AST/AbsyCmd.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Diagnostics;
 using System.Collections.Generic;
+using System.ComponentModel;
 using System.Linq;
 using System.Diagnostics.Contracts;
 using Set = Microsoft.Boogie.GSet<object>;
@@ -3333,48 +3334,36 @@ public override Absy StdDispatch(StandardVisitor visitor)
 
   public class HavocCmd : Cmd
   {
-    private List<IdentifierExpr> /*!*/ _vars;
+    public List<IdentifierExpr> /*!*/ VarsIncludingMonotonic { get; set; }
 
-    public List<IdentifierExpr> /*!*/ Vars
-    {
-      get
-      {
-        Contract.Ensures(Contract.Result<List<IdentifierExpr>>() != null);
-        return this._vars;
-      }
-      set
-      {
-        Contract.Requires(value != null);
-        this._vars = value;
-      }
-    }
+    public IEnumerable<IdentifierExpr> /*!*/ Vars => VarsIncludingMonotonic.Where(v => !v.Decl.Monotonic);
 
     [ContractInvariantMethod]
     void ObjectInvariant()
     {
-      Contract.Invariant(this._vars != null);
+      Contract.Invariant(this.VarsIncludingMonotonic != null);
     }
 
     public HavocCmd(IToken /*!*/ tok, List<IdentifierExpr> /*!*/ vars)
       : base(tok)
     {
       Contract.Requires(tok != null);
       Contract.Requires(vars != null);
-      this._vars = vars;
+      this.VarsIncludingMonotonic = vars;
     }
 
     public override void Emit(TokenTextWriter stream, int level)
     {
       //Contract.Requires(stream != null);
       stream.Write(this, level, "havoc ");
-      Vars.Emit(stream, true);
+      VarsIncludingMonotonic.Emit(stream, true);
       stream.WriteLine(";");
     }
 
     public override void Resolve(ResolutionContext rc)
     {
       //Contract.Requires(rc != null);
-      foreach (IdentifierExpr /*!*/ ide in Vars)
+      foreach (IdentifierExpr /*!*/ ide in VarsIncludingMonotonic)
       {
         Contract.Assert(ide != null);
         ide.Resolve(rc);
@@ -3392,7 +3381,7 @@ public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
     public override void Typecheck(TypecheckingContext tc)
     {
       //Contract.Requires(tc != null);
-      foreach (IdentifierExpr ie in Vars)
+      foreach (IdentifierExpr ie in VarsIncludingMonotonic)
       {
         ie.Typecheck(tc);
       }

Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs

@@ -134,10 +134,8 @@ public void Propagate(Cmd cmd, HashSet<Variable /*!*/> /*!*/ liveSet)
         index++;
       }
     }
-    else if (cmd is HavocCmd)
+    else if (cmd is HavocCmd havocCmd)
     {
-      HavocCmd /*!*/
-        havocCmd = (HavocCmd) cmd;
       foreach (IdentifierExpr /*!*/ expr in havocCmd.Vars)
       {
         Contract.Assert(expr != null);

Source/Core/BoogiePL.atg

@@ -265,10 +265,14 @@ LocalVars<.List<Variable>/*!*/ ds.>
 = (.
     Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
     QKeyValue kv = null;
+    bool monotonic = false;
   .)
+  [ "monotonic" (. monotonic = true; .) ] 
   "var"
   { Attribute<ref kv> }
-  IdsTypeWheres<true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } > ";"
+  IdsTypeWheres<true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv) {
+    Monotonic = monotonic 
+  }); } > ";"
   .
 
 ProcFormals<.bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds.>