Merging changes from 0biha/BoogieInvariantFixesII

5 files changed, 199 insertions, 42 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index f348c788..7622cbdf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -38,15 +38,27 @@ namespace Microsoft.Boogie.AbstractInterpretation {
   }

 

   public class ProcedureSummaryEntry {

-    public HashSet<CallSite>/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

+

+    private HashSet<CallSite>/*!*/ _returnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

+

+    public HashSet<CallSite>/*!*/ ReturnPoints {

+      get {

+        Contract.Ensures(Contract.Result<HashSet<CallSite>>() != null);

+        return this._returnPoints;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._returnPoints = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(ReturnPoints != null);

+      Contract.Invariant(this._returnPoints != null);

     }

 

-

     public ProcedureSummaryEntry() {

-      this.ReturnPoints = new HashSet<CallSite>();

+      this._returnPoints = new HashSet<CallSite>();

     }

 

   } // class

@@ -2856,10 +2868,23 @@ namespace Microsoft.Boogie {
 

   public class Ensures : Absy, IPotentialErrorNode {

     public readonly bool Free;

-    public Expr/*!*/ Condition;

+

+    private Expr/*!*/ _condition;

+ 	  

+ 	  public Expr/*!*/ Condition {

+ 	    get {

+ 	      Contract.Ensures(Contract.Result<Expr>() != null);

+ 	      return this._condition;

+ 	    }

+ 	    set {

+ 	      Contract.Requires(value != null);

+ 	      this._condition = value;

+ 	    }

+ 	  }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Condition != null);

+      Contract.Invariant(this._condition != null); 

       Contract.Invariant(errorData == null || errorData is string);

     }

 

@@ -2899,7 +2924,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(condition != null);

       Contract.Requires(token != null);

       this.Free = free;

-      this.Condition = condition;

+      this._condition = condition; 

       this.Comment = comment;

       this.Attributes = kv;

     }

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 3b369863..231ae272 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1269,22 +1269,64 @@ namespace Microsoft.Boogie {
   // class for parallel assignments, which subsumes both the old

   // SimpleAssignCmd and the old MapAssignCmd

   public class AssignCmd : Cmd {

-    public List<AssignLhs/*!*/>/*!*/ Lhss;

-    public List<Expr/*!*/>/*!*/ Rhss;

+    private List<AssignLhs/*!*/>/*!*/ _lhss;

+

+    public IList<AssignLhs/*!*/>/*!*/ Lhss {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<AssignLhs>>()));

+        Contract.Ensures(Contract.Result<IList<AssignLhs>>().IsReadOnly);

+        return this._lhss.AsReadOnly();

+      }

+      set {

+        Contract.Requires(cce.NonNullElements(value));

+        this._lhss = new List<AssignLhs>(value);

+      }

+    }

+

+    internal void SetLhs(int index, AssignLhs lhs)

+    {

+      Contract.Requires(0 <= index && index < this.Lhss.Count);

+      Contract.Requires(lhs != null);

+      Contract.Ensures(this.Lhss[index] == lhs);

+      this._lhss[index] = lhs;

+    }
+
+    private List<Expr/*!*/>/*!*/ _rhss;

+

+    public IList<Expr/*!*/>/*!*/ Rhss {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<Expr>>()));

+        Contract.Ensures(Contract.Result<IList<Expr>>().IsReadOnly);

+        return this._rhss.AsReadOnly();

+      }

+      set {

+        Contract.Requires(cce.NonNullElements(value));

+        this._rhss = new List<Expr>(value);

+      }

+    }

+

+    internal void SetRhs(int index, Expr rhs)

+    {

+      Contract.Requires(0 <= index && index < this.Rhss.Count);

+      Contract.Requires(rhs != null);

+      Contract.Ensures(this.Rhss[index] == rhs);

+      this._rhss[index] = rhs;

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(Lhss));

-      Contract.Invariant(cce.NonNullElements(Rhss));

+      Contract.Invariant(cce.NonNullElements(this._lhss));

+      Contract.Invariant(cce.NonNullElements(this._rhss));

     }

 

 

-    public AssignCmd(IToken tok, List<AssignLhs/*!*/>/*!*/ lhss, List<Expr/*!*/>/*!*/ rhss)

+    public AssignCmd(IToken tok, IList<AssignLhs/*!*/>/*!*/ lhss, IList<Expr/*!*/>/*!*/ rhss)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(rhss));

       Contract.Requires(cce.NonNullElements(lhss));

-      Lhss = lhss;

-      Rhss = rhss;

+      this._lhss = new List<AssignLhs>(lhss);

+      this._rhss = new List<Expr>(rhss);

     }

 

     public override void Emit(TokenTextWriter stream, int level) {

@@ -1698,20 +1740,43 @@ namespace Microsoft.Boogie {
   public class StateCmd : Cmd {

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Locals != null);

-      Contract.Invariant(Cmds != null);

+      Contract.Invariant(this._locals != null);

+      Contract.Invariant(this._cmds != null);

     }

 

-    public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals;

-    public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds;

+    private List<Variable> _locals;

+

+    public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals {

+      get {

+        Contract.Ensures(Contract.Result<List<Variable>>() != null);

+        return this._locals;

+      }

+      internal set {

+        Contract.Requires(value != null);

+        this._locals = value;

+      }

+    }

+

+    private List<Cmd> _cmds;

+

+    public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds {

+      get {

+        Contract.Ensures(Contract.Result<List<Cmd>>() != null);

+        return this._cmds;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._cmds = value;

+      }

+    }

 

     public StateCmd(IToken tok, List<Variable>/*!*/ locals, List<Cmd>/*!*/ cmds)

       : base(tok) {

       Contract.Requires(locals != null);

       Contract.Requires(cmds != null);

       Contract.Requires(tok != null);

-      this.Locals = locals;

-      this.Cmds = cmds;

+      this._locals = locals;

+      this._cmds = cmds;

     }

 

     public override void Resolve(ResolutionContext rc) {

@@ -2959,18 +3024,31 @@ namespace Microsoft.Boogie {
   }

 

   public class HavocCmd : Cmd {

-    public List<IdentifierExpr>/*!*/ Vars;

+    private List<IdentifierExpr>/*!*/ _vars;

+

+    public List<IdentifierExpr>/*!*/ Vars {

+      get {

+        Contract.Ensures(Contract.Result<List<IdentifierExpr>>() != null);

+        return this._vars;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._vars = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Vars != null);

+      Contract.Invariant(this._vars != null);

     }

 

     public HavocCmd(IToken/*!*/ tok, List<IdentifierExpr>/*!*/ vars)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(vars != null);

-      Vars = vars;

+      this._vars = vars;

     }

+

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

       stream.Write(this, level, "havoc ");

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 682e058c..35e1edc9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -17,16 +17,39 @@ namespace Microsoft.Boogie {
   {

     public readonly string ToolName;

     public readonly string DescriptiveToolName;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(ToolName != null);

       Contract.Invariant(DescriptiveToolName != null);

-      Contract.Invariant(Environment != null);

-      Contract.Invariant(cce.NonNullElements(Files));

+      Contract.Invariant(this._environment != null);

+      Contract.Invariant(cce.NonNullElements(this._files));

+      Contract.Invariant(this._fileTimestamp != null);

+    }

+

+    private string/*!*/ _environment = "";

+

+    public string Environment {

+      get {

+        Contract.Ensures(Contract.Result<string>() != null);

+        return this._environment;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._environment = value;

+      }

+    }

+

+    private readonly List<string/*!*/>/*!*/ _files = new List<string/*!*/>();

+

+    public IList<string/*!*/>/*!*/ Files {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<string>>()));

+        Contract.Ensures(Contract.Result<IList<string>>().IsReadOnly);

+        return this._files.AsReadOnly();

+      }

     }

 

-    public string/*!*/ Environment = "";

-    public List<string/*!*/>/*!*/ Files = new List<string/*!*/>();

     public bool HelpRequested = false;

     public bool AttrHelpRequested = false;

 

@@ -56,7 +79,19 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public string/*!*/ FileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');

+    private string/*!*/ _fileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');

+

+    public string FileTimestamp {

+      get {

+        Contract.Ensures(Contract.Result<string>() != null);

+        return this._fileTimestamp;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._fileTimestamp = value;

+      }

+    }

+

     public void ExpandFilename(ref string pattern, string logPrefix, string fileTimestamp) {

       if (pattern != null) {

         pattern = pattern.Replace("@PREFIX@", logPrefix).Replace("@TIME@", fileTimestamp);

@@ -302,12 +337,12 @@ namespace Microsoft.Boogie {
         if (isOption) {

           if (!ParseOption(ps.s.Substring(1), ps)) {

             if (Path.DirectorySeparatorChar == '/' && ps.s.StartsWith("/"))

-              Files.Add(arg);

+              this._files.Add(arg);

             else

               ps.Error("unknown switch: {0}", ps.s);

           }

         } else {

-          Files.Add(arg);

+          this._files.Add(arg);

         }

 

         ps.i = ps.nextIndex;

@@ -336,10 +371,6 @@ namespace Microsoft.Boogie {
   /// superset of Boogie's options.

   /// </summary>

   public class CommandLineOptions : CommandLineOptionEngine {

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(FileTimestamp != null);

-    }

 

     public CommandLineOptions()

       : base("Boogie", "Boogie program verifier") {

@@ -383,7 +414,6 @@ namespace Microsoft.Boogie {
     public bool DoomRestartTP = false;

     public bool PrintDesugarings = false;

     public string SimplifyLogFilePath = null;

-    public string/*!*/ LogPrefix = "";

     public bool PrintInstrumented = false;

     public bool InstrumentWithAsserts = false;

     public enum InstrumentationPlaces {

@@ -432,6 +462,19 @@ namespace Microsoft.Boogie {
     public string CVC4ExecutablePath = null;

     public int KInductionDepth = -1;

 

+    private string/*!*/ _logPrefix = "";

+

+    public string LogPrefix {

+      get {

+        Contract.Ensures(Contract.Result<string>() != null);

+        return this._logPrefix;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._logPrefix = value;

+      }

+    }

+

     public bool PrettyPrint = true;

 

     public enum ProverWarnings {

@@ -668,7 +711,7 @@ namespace Microsoft.Boogie {
       public bool J_Intervals = false;

       public bool DebugStatistics = false;

     }

-    public AiFlags/*!*/ Ai = new AiFlags();

+    public readonly AiFlags/*!*/ Ai = new AiFlags();

 

     public class ConcurrentHoudiniOptions

     {

diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 5b5c0306..b23a46a4 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -217,7 +217,7 @@ public class Scanner {
 

 	[ContractInvariantMethod]

 	void objectInvariant(){

-		Contract.Invariant(buffer!=null);

+		Contract.Invariant(this._buffer != null);

 		Contract.Invariant(t != null);

 		Contract.Invariant(start != null);

 		Contract.Invariant(tokens != null);

@@ -227,7 +227,18 @@ public class Scanner {
 		Contract.Invariant(errorHandler != null);

 	}

 

-	public Buffer/*!*/ buffer; // scanner buffer

+	private Buffer/*!*/ _buffer; // scanner buffer

+

+	public Buffer/*!*/ buffer {

+		get {

+			Contract.Ensures(Contract.Result<Buffer>() != null);

+			return this._buffer;

+		}

+		set {

+			Contract.Requires(value != null);

+			this._buffer = value;

+		}

+	}

 

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

@@ -304,7 +315,7 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

-			buffer = new Buffer(stream, false);

+			this._buffer = new Buffer(stream, false);

 			Filename = useBaseName? GetBaseName(fileName): fileName;

 			Init();

 		} catch (IOException) {

@@ -319,7 +330,7 @@ public class Scanner {
 	  Contract.Requires(fileName != null);

 		pt = tokens = new Token();  // first token is a dummy

 		t = new Token(); // dummy because t is a non-null field

-		buffer = new Buffer(s, true);

+		this._buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

 		Init();

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 3f3ad5ae..98ea4df3 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -75,8 +75,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);

       for (int i = 0; i < node.Lhss.Count; ++i) {

-        node.Lhss[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));

-        node.Rhss[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));

+        node.SetLhs(i, cce.NonNull((AssignLhs)this.Visit(node.Lhss[i])));

+        node.SetRhs(i, cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i])));

       }

       return node;

     }