diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 43 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 6 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 |
3 files changed, 31 insertions, 20 deletions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index cb792421..96e74b80 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -416,32 +416,43 @@ namespace Microsoft.Boogie { public class Trigger : Absy {
public readonly bool Pos;
[Rep]
- public List<Expr>/*!*/ Tr;
+ private List<Expr>/*!*/ tr;
+
+ public IList<Expr>/*!*/ Tr
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<IList<Expr>>() != null);
+ Contract.Ensures(Contract.Result<IList<Expr>>().Count >= 1);
+ Contract.Ensures(this.Pos || Contract.Result<IList<Expr>>().Count == 1);
+ return this.tr.AsReadOnly();
+ }
+ set
+ {
+ Contract.Requires(value != null);
+ Contract.Requires(value.Count >= 1);
+ Contract.Requires(this.Pos || value.Count == 1);
+ this.tr = new List<Expr>(value);
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Tr != null);
- Contract.Invariant(1 <= Tr.Count);
- Contract.Invariant(Pos || Tr.Count == 1);
+ Contract.Invariant(this.tr != null);
+ Contract.Invariant(this.tr.Count >= 1);
+ Contract.Invariant(Pos || this.tr.Count == 1);
}
public Trigger Next;
- public Trigger(IToken tok, bool pos, List<Expr> tr)
- : this(tok, pos, tr, null) {
- Contract.Requires(tr != null);
- Contract.Requires(tok != null);
- Contract.Requires(1 <= tr.Count);
- Contract.Requires(pos || tr.Count == 1);
- }
-
- public Trigger(IToken/*!*/ tok, bool pos, List<Expr>/*!*/ tr, Trigger next)
+ public Trigger(IToken/*!*/ tok, bool pos, IEnumerable<Expr>/*!*/ tr, Trigger next = null)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(tr != null);
- Contract.Requires(1 <= tr.Count);
- Contract.Requires(pos || tr.Count == 1);
+ Contract.Requires(tr.Count() >= 1);
+ Contract.Requires(pos || tr.Count() == 1);
this.Pos = pos;
- this.Tr = tr;
+ this.Tr = new List<Expr>(tr);
this.Next = next;
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 68de45f6..abd106a5 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -523,11 +523,11 @@ namespace Microsoft.Boogie { if (origNext != null) {
Trigger newNext = this.VisitTrigger(origNext);
if (newNext != origNext) {
- node = new Trigger(node.tok, node.Pos, node.Tr); // note: this creates sharing between the old and new Tr sequence
+ node = new Trigger(node.tok, node.Pos, node.Tr.ToList());
node.Next = newNext;
}
}
- node.Tr = this.VisitExprSeq(node.Tr);
+ node.Tr = this.VisitExprSeq(node.Tr.ToList());
return node;
}
// called by default for all nullary type constructors and type variables
@@ -1073,7 +1073,7 @@ namespace Microsoft.Boogie { {
this.VisitTrigger(origNext);
}
- this.VisitExprSeq(node.Tr);
+ this.VisitExprSeq(node.Tr.ToList());
return node;
}
// called by default for all nullary type constructors and type variables
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index a9963b72..91c17b23 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -76,7 +76,7 @@ namespace Microsoft.Boogie.VCExprAST { return Pop();
}
- public List<VCExpr/*!*/>/*!*/ Translate(List<Expr> exprs) {
+ public List<VCExpr/*!*/>/*!*/ Translate(IList<Expr> exprs) {
Contract.Requires(exprs != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
|