From 217b0584ba0008d019e35f4e8249c3e62bbefa3a Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Thu, 8 Jan 2015 01:53:23 +0100
Subject: Made invariant of class 'CommandLineOptions' robust by changing the
 design (replaced public variable by private variable + getter/setter).

---
 Source/Core/CommandLineOptions.cs | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

(limited to 'Source')

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": {
-- 
cgit v1.2.3