Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.

4 files changed, 37 insertions, 27 deletions

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;

     }