Made invariant of class 'CommandLineOptions' robust by changing the design

(replaced public variable by private variable + getter/setter).

1 files changed, 17 insertions, 3 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 35e1edc9..41ea4d03 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -218,6 +218,7 @@ namespace Microsoft.Boogie {
       /// </summary>

       public bool GetNumericArgument(ref int arg, int limit) {

         Contract.Requires(this.i < args.Length);

+        Contract.Ensures(Math.Min(arg, 0) <= Contract.ValueAtReturn(out arg) && Contract.ValueAtReturn(out arg) < limit);

         //modifies nextIndex, encounteredErrors, Console.Error.*;

         int a = arg;

         if (!GetNumericArgument(ref a)) {

@@ -236,6 +237,7 @@ namespace Microsoft.Boogie {
       /// Otherwise, emit an error message, leave "arg" unchanged, and return "false".

       /// </summary>

       public bool GetNumericArgument(ref double arg) {

+        Contract.Ensures(Contract.ValueAtReturn(out arg) >= 0);

         //modifies nextIndex, encounteredErrors, Console.Error.*;

         if (this.ConfirmArgumentCount(1)) {

           try {

@@ -508,7 +510,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);

       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);

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

-      Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC < 2);

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

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

     }

 

@@ -575,7 +577,19 @@ namespace Microsoft.Boogie {
     [Peer]

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

 

-    public int BracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes

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

+

+    public int BracketIdsInVC {

+      get {

+        Contract.Ensures(-1 <= Contract.Result<int>() && Contract.Result<int>() <= 1);

+        return this.bracketIdsInVC;

+      }

+      set {

+        Contract.Requires(-1 <= value && value <= 1);

+        this.bracketIdsInVC = value;

+      }

+    }

+

     public bool CausalImplies = false;

 

     public int SimplifyProverMatchDepth = -1;  // -1 means not specified

@@ -1296,7 +1310,7 @@ namespace Microsoft.Boogie {
           return true;

 

         case "vcBrackets":

-          ps.GetNumericArgument(ref BracketIdsInVC, 2);

+          ps.GetNumericArgument(ref bracketIdsInVC, 2);

           return true;

 

         case "proverMemoryLimit": {