Merging changes from wuestholz/BoogieInvariantFixesIIII

1 files changed, 58 insertions, 12 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ca08072..072e0323 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------

+//-----------------------------------------------------------------------------

 //

 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

@@ -511,7 +511,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);

       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);

       Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1);

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

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

     }

 

     public int LoopUnrollCount = -1;  // -1 means don't unroll loops

@@ -589,7 +589,28 @@ namespace Microsoft.Boogie {
     public ProverFactory TheProverFactory;

     public string ProverName;

     [Peer]

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

+    private List<string> proverOptions = new List<string>();

+

+    public IEnumerable<string> ProverOptions

+    {

+      get

+      {

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

+        foreach (string s in this.proverOptions)

+          yield return s;

+      }

+    }

+

+    public void AddProverOption(string option)

+    {

+      Contract.Requires(option != null);

+      this.proverOptions.Add(option);

+    }

+

+    public void RemoveAllProverOptions(Predicate<string> match)

+    {

+      this.proverOptions.RemoveAll(match);

+    }

 

     private int bracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes

 

@@ -637,12 +658,29 @@ namespace Microsoft.Boogie {
     }

     [ContractInvariantMethod]

     void ObjectInvariant4() {

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

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

       Contract.Invariant(0 <= Z3lets && Z3lets < 4);

     }

 

     [Peer]

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

+    private List<string> z3Options = new List<string>();

+

+    public IEnumerable<string> Z3Options

+    {

+      get

+      {

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

+        foreach (string s in z3Options)

+          yield return s;

+      }

+    }

+

+    public void AddZ3Option(string option)

+    {

+      Contract.Requires(option != null);

+      this.z3Options.Add(option);

+    }

+

     public bool Z3types = false;

     public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any

 

@@ -727,10 +765,18 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public List<string/*!*/> ProcsToCheck = null;  // null means "no restriction"

+    public IEnumerable<string/*!*/> ProcsToCheck {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>>(), true));

+        return this.procsToCheck != null ? this.procsToCheck.AsEnumerable() : null;

+      }

+    }

+

+    private List<string/*!*/> procsToCheck = null;  // null means "no restriction"

+    

     [ContractInvariantMethod]

     void ObjectInvariant5() {

-      Contract.Invariant(cce.NonNullElements(ProcsToCheck, true));

+      Contract.Invariant(cce.NonNullElements(this.procsToCheck, true));

       Contract.Invariant(Ai != null);

     }

 

@@ -804,11 +850,11 @@ namespace Microsoft.Boogie {
           return true;

 

         case "proc":

-          if (ProcsToCheck == null) {

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

+          if (this.procsToCheck == null) {

+            this.procsToCheck = new List<string/*!*/>();

           }

           if (ps.ConfirmArgumentCount(1)) {

-            ProcsToCheck.Add(cce.NonNull(args[ps.i]));

+            this.procsToCheck.Add(cce.NonNull(args[ps.i]));

           }

           return true;

 

@@ -1127,7 +1173,7 @@ namespace Microsoft.Boogie {
         case "p":

         case "proverOpt":

           if (ps.ConfirmArgumentCount(1)) {

-            ProverOptions.Add(cce.NonNull(args[ps.i]));

+            AddProverOption(cce.NonNull(args[ps.i]));

           }

           return true;

 

@@ -1420,7 +1466,7 @@ namespace Microsoft.Boogie {
 		

         case "z3opt":

           if (ps.ConfirmArgumentCount(1)) {

-            Z3Options.Add(cce.NonNull(args[ps.i]));

+            AddZ3Option(cce.NonNull(args[ps.i]));

           }

           return true;