From 2adff68a1579de5ba40c8b8713fc75a383e1ff91 Mon Sep 17 00:00:00 2001 From: wuestholz 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 ProverOptions { + set + { + Contract.Requires(cce.NonNullElements(value)); + + this.proverOptions = new List(value); + } get { - Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + 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 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() != null); + Contract.Ensures(Contract.Result() != null); return base.VisitBvConcatExpr((BvConcatExpr) node.Clone()); } public override Expr VisitBvExtractExpr(BvExtractExpr node) { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != null); return base.VisitExistsExpr((ExistsExpr)node.Clone()); } public override Expr VisitExpr(Expr node) { @@ -216,12 +216,12 @@ namespace Microsoft.Boogie { } public override IList VisitExprSeq(IList list) { //Contract.Requires(list != null); - Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>() != null); return base.VisitExprSeq(new List(list)); } public override Expr VisitForallExpr(ForallExpr node) { //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != 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 VisitExprSeq(IList list) { Contract.Requires(list != null); - Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>() != 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() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != null); node = (ExistsExpr)this.VisitQuantifierExpr(node); return node; } public virtual Expr VisitBvExtractExpr(BvExtractExpr node) { Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); node.Bitvector = this.VisitExpr(node.Bitvector); return node; } @@ -259,7 +259,7 @@ namespace Microsoft.Boogie { } public override IList VisitExprSeq(IList exprSeq) { //Contract.Requires(exprSeq != null); - Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>() != 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() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != null); return node; } @@ -681,7 +681,7 @@ namespace Microsoft.Boogie { } public override Expr VisitBvConcatExpr(BvConcatExpr node) { - Contract.Ensures(Contract.Result() == node); + Contract.Ensures(Contract.Result() == 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() == node); + Contract.Ensures(Contract.Result() == node); return (ExistsExpr)this.VisitQuantifierExpr(node); } public override Expr VisitBvExtractExpr(BvExtractExpr node) { - Contract.Ensures(Contract.Result() == node); + Contract.Ensures(Contract.Result() == node); this.VisitExpr(node.Bitvector); return node; } @@ -823,7 +823,7 @@ namespace Microsoft.Boogie { } public override IList VisitExprSeq(IList exprSeq) { - Contract.Ensures(Contract.Result>() == exprSeq); + Contract.Ensures(Contract.Result>() == 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() == node); + Contract.Ensures(Contract.Result() == 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() == node); + Contract.Ensures(Contract.Result() == 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() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != null); node = (ExistsExpr)this.VisitQuantifierExpr(node); return node; } public override Expr VisitForallExpr(ForallExpr node) { //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != 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() != null); + Contract.Ensures(Contract.Result() != null); Push(TranslateBvConcatExpr(node)); return node; } -- cgit v1.2.3 From 057555507c62120356f8eb22f7ec050c47983ad4 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Wed, 18 Feb 2015 13:24:48 +0100 Subject: Eliminated calls to deprecated method. --- Source/Core/CommandLineOptions.cs | 2 +- Source/Houdini/AbstractHoudini.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index bd4c7a91..bbdccda9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1204,7 +1204,7 @@ namespace Microsoft.Boogie { case "p": case "proverOpt": if (ps.ConfirmArgumentCount(1)) { - AddProverOption(cce.NonNull(args[ps.i])); + ProverOptions = ProverOptions.Concat1(cce.NonNull(args[ps.i])); } return true; diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index b49107a0..de3d3779 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -2199,7 +2199,7 @@ namespace Microsoft.Boogie.Houdini { this.name2Impl = SimpleUtil.nameImplMapping(program); if (CommandLineOptions.Clo.ProverKillTime > 0) - CommandLineOptions.Clo.AddProverOption(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); + CommandLineOptions.Clo.ProverOptions = CommandLineOptions.Clo.ProverOptions.Concat1(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime)); this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List()); this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1); -- cgit v1.2.3