From 2adff68a1579de5ba40c8b8713fc75a383e1ff91 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 18 Feb 2015 13:14:26 +0100
Subject: Added a setter for CommandLineOptions.ProverOptions and fixed several
 contracts.

---
 Source/Core/CommandLineOptions.cs | 16 +++++++++++++---
 Source/Core/Duplicator.cs         | 12 ++++++------
 Source/Core/StandardVisitor.cs    | 26 +++++++++++++-------------
 Source/VCExpr/Boogie2VCExpr.cs    | 10 +++++-----
 4 files changed, 37 insertions(+), 27 deletions(-)

(limited to 'Source')

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 3559e0c9..bd4c7a91 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -614,23 +614,33 @@ namespace Microsoft.Boogie {
 
     public IEnumerable<string> ProverOptions
     {
+      set
+      {
+        Contract.Requires(cce.NonNullElements(value));
+
+        this.proverOptions = new List<string>(value);
+      }
       get
       {
-        Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>()));
+
         foreach (string s in this.proverOptions)
           yield return s;
       }
     }
 
+    [Obsolete("use the setter for 'ProverOptions' directly")]
     public void AddProverOption(string option)
     {
       Contract.Requires(option != null);
-      this.proverOptions.Add(option);
+
+      this.ProverOptions = this.ProverOptions.Concat1(option);
     }
 
+    [Obsolete("use the setter for 'ProverOptions' directly")]
     public void RemoveAllProverOptions(Predicate<string> match)
     {
-      this.proverOptions.RemoveAll(match);
+      this.ProverOptions = this.ProverOptions.Where(s => !match(s));
     }
 
     private int bracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index becd1791..181b80a1 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -78,11 +78,11 @@ namespace Microsoft.Boogie {
       return base.VisitBlock((Block) node.Clone());
     }
     public override Expr VisitBvConcatExpr (BvConcatExpr node) {
-      Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       return base.VisitBvConcatExpr((BvConcatExpr) node.Clone());
     }
     public override Expr VisitBvExtractExpr(BvExtractExpr node) {
-      Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       return base.VisitBvExtractExpr((BvExtractExpr) node.Clone());
     }
     public override Expr VisitCodeExpr(CodeExpr node) {
@@ -206,7 +206,7 @@ namespace Microsoft.Boogie {
     }
     public override Expr VisitExistsExpr(ExistsExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<ExistsExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       return base.VisitExistsExpr((ExistsExpr)node.Clone());
     }
     public override Expr VisitExpr(Expr node) {
@@ -216,12 +216,12 @@ namespace Microsoft.Boogie {
     }
     public override IList<Expr> VisitExprSeq(IList<Expr> list) {
       //Contract.Requires(list != null);
-      Contract.Ensures(Contract.Result<List<Expr>>() != null);
+      Contract.Ensures(Contract.Result<IList<Expr>>() != null);
       return base.VisitExprSeq(new List<Expr>(list));
     }
     public override Expr VisitForallExpr(ForallExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<ForallExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       return base.VisitForallExpr((ForallExpr)node.Clone());
     }
     public override Formal VisitFormal(Formal node) {
@@ -292,7 +292,7 @@ namespace Microsoft.Boogie {
     }
     public override Expr VisitLiteralExpr(LiteralExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       return base.VisitLiteralExpr((LiteralExpr)node.Clone());
     }
     public override LocalVariable VisitLocalVariable(LocalVariable node) {
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 8c3d6326..0323d4db 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -32,7 +32,7 @@ namespace Microsoft.Boogie {
 
     public virtual IList<Expr> VisitExprSeq(IList<Expr> list) {
       Contract.Requires(list != null);
-      Contract.Ensures(Contract.Result<List<Expr>>() != null);
+      Contract.Ensures(Contract.Result<IList<Expr>>() != null);
       lock (list)
       {
         for (int i = 0, n = list.Count; i < n; i++)
@@ -105,7 +105,7 @@ namespace Microsoft.Boogie {
     }
     public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {
       Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       node.E0 = this.VisitExpr(node.E0);
       node.E1 = this.VisitExpr(node.E1);
       return node;
@@ -241,13 +241,13 @@ namespace Microsoft.Boogie {
     }
     public virtual Expr VisitExistsExpr(ExistsExpr node) {
       Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<ExistsExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       node = (ExistsExpr)this.VisitQuantifierExpr(node);
       return node;
     }
     public virtual Expr VisitBvExtractExpr(BvExtractExpr node) {
       Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       node.Bitvector = this.VisitExpr(node.Bitvector);
       return node;
     }
@@ -259,7 +259,7 @@ namespace Microsoft.Boogie {
     }
     public override IList<Expr> VisitExprSeq(IList<Expr> exprSeq) {
       //Contract.Requires(exprSeq != null);
-      Contract.Ensures(Contract.Result<List<Expr>>() != null);
+      Contract.Ensures(Contract.Result<IList<Expr>>() != null);
       for (int i = 0, n = exprSeq.Count; i < n; i++)
         exprSeq[i] = this.VisitExpr(cce.NonNull(exprSeq[i]));
       return exprSeq;
@@ -292,7 +292,7 @@ namespace Microsoft.Boogie {
     }
     public virtual Expr VisitForallExpr(ForallExpr node) {
       Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<ForallExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       node = (ForallExpr)this.VisitQuantifierExpr(node);
       return node;
     }
@@ -361,7 +361,7 @@ namespace Microsoft.Boogie {
     }
     public virtual Expr VisitLiteralExpr(LiteralExpr node) {
       Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       return node;
     }
 
@@ -681,7 +681,7 @@ namespace Microsoft.Boogie {
       }
       public override Expr VisitBvConcatExpr(BvConcatExpr node)
       {
-          Contract.Ensures(Contract.Result<BvConcatExpr>() == node);
+          Contract.Ensures(Contract.Result<Expr>() == node);
           this.VisitExpr(node.E0);
           this.VisitExpr(node.E1);
           return node;
@@ -807,12 +807,12 @@ namespace Microsoft.Boogie {
       }
       public override Expr VisitExistsExpr(ExistsExpr node)
       {
-          Contract.Ensures(Contract.Result<ExistsExpr>() == node);
+          Contract.Ensures(Contract.Result<Expr>() == node);
           return (ExistsExpr)this.VisitQuantifierExpr(node);
       }
       public override Expr VisitBvExtractExpr(BvExtractExpr node)
       {
-          Contract.Ensures(Contract.Result<BvExtractExpr>() == node);
+          Contract.Ensures(Contract.Result<Expr>() == node);
           this.VisitExpr(node.Bitvector);
           return node;
       }
@@ -823,7 +823,7 @@ namespace Microsoft.Boogie {
       }
       public override IList<Expr> VisitExprSeq(IList<Expr> exprSeq)
       {
-          Contract.Ensures(Contract.Result<List<Expr>>() == exprSeq);
+          Contract.Ensures(Contract.Result<IList<Expr>>() == exprSeq);
           for (int i = 0, n = exprSeq.Count; i < n; i++)
               this.VisitExpr(cce.NonNull(exprSeq[i]));
           return exprSeq;
@@ -856,7 +856,7 @@ namespace Microsoft.Boogie {
       }
       public override Expr VisitForallExpr(ForallExpr node)
       {
-          Contract.Ensures(Contract.Result<ForallExpr>() == node);
+          Contract.Ensures(Contract.Result<Expr>() == node);
           return (ForallExpr)this.VisitQuantifierExpr(node);
       }
       public override Expr VisitLambdaExpr(LambdaExpr node) {
@@ -917,7 +917,7 @@ namespace Microsoft.Boogie {
       }
       public override Expr VisitLiteralExpr(LiteralExpr node)
       {
-          Contract.Ensures(Contract.Result<LiteralExpr>() == node);
+          Contract.Ensures(Contract.Result<Expr>() == node);
           return node;
       }
 
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 49dbb7c8..8674f8c0 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -316,7 +316,7 @@ namespace Microsoft.Boogie.VCExprAST {
 
     public override Expr VisitLiteralExpr(LiteralExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       Push(TranslateLiteralExpr(node));
       return node;
     }
@@ -456,14 +456,14 @@ namespace Microsoft.Boogie.VCExprAST {
 
     public override Expr VisitExistsExpr(ExistsExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<ExistsExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       node = (ExistsExpr)this.VisitQuantifierExpr(node);
       return node;
     }
 
     public override Expr VisitForallExpr(ForallExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<ForallExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       node = (ForallExpr)this.VisitQuantifierExpr(node);
       return node;
     }
@@ -559,7 +559,7 @@ namespace Microsoft.Boogie.VCExprAST {
 
     public override Expr VisitBvExtractExpr(BvExtractExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       Push(TranslateBvExtractExpr(node));
       return node;
     }
@@ -576,7 +576,7 @@ namespace Microsoft.Boogie.VCExprAST {
 
     public override Expr VisitBvConcatExpr(BvConcatExpr node) {
       //Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
+      Contract.Ensures(Contract.Result<Expr>() != null);
       Push(TranslateBvConcatExpr(node));
       return node;
     }
-- 
cgit v1.2.3