diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 22:30:46 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 22:30:46 +0100 |
| commit | 793c0c0ded44401a1d6ef1bf494dd0a3d0b8dc43 (patch) | |
| tree | 2187085433b50195a7e2783e27d0386187806378 /Source | |
| parent | 48731a5c9679efa8bcf7920c279108927a85f2f1 (diff) | |
RESeq: farewell
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 16 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 6 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 4 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 4 |
4 files changed, 10 insertions, 20 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index fa601737..23935658 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3361,16 +3361,6 @@ namespace Microsoft.Boogie { #region Regular Expressions
// a data structure to recover the "program structure" from the flow graph
- public sealed class RESeq : List<RE> {
- public RESeq(params RE[] args)
- : base(args) {
- Contract.Requires(args != null);
- }
- public RESeq(RESeq reSeq)
- : base(reSeq) {
- Contract.Requires(reSeq != null);
- }
- }
public abstract class RE : Cmd {
public RE()
: base(Token.NoToken) {
@@ -3455,8 +3445,8 @@ namespace Microsoft.Boogie { Contract.Invariant(rs != null);
}
- public RESeq/*!*/ rs;
- public Choice(RESeq operands) {
+ public List<RE>/*!*/ rs;
+ public Choice(List<RE> operands) {
Contract.Requires(operands != null);
rs = operands;
}
@@ -3490,7 +3480,7 @@ namespace Microsoft.Boogie { if (g.labelTargets.Count == 1) {
return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.labelTargets[0])));
} else {
- RESeq rs = new RESeq();
+ List<RE> rs = new List<RE>();
foreach (Block/*!*/ target in g.labelTargets) {
Contract.Assert(target != null);
RE r = Transform(target);
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 3355c9a0..2d220a35 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -262,10 +262,10 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Cmd>() != null);
return base.VisitRE((RE)node.Clone());
}
- public override RESeq VisitRESeq(RESeq reSeq) {
+ public override List<RE> VisitRESeq(List<RE> reSeq) {
//Contract.Requires(reSeq != null);
- Contract.Ensures(Contract.Result<RESeq>() != null);
- return base.VisitRESeq(new RESeq(reSeq));
+ Contract.Ensures(Contract.Result<List<RE>>() != null);
+ return base.VisitRESeq(new List<RE>(reSeq));
}
public override ReturnCmd VisitReturnCmd(ReturnCmd node) {
//Contract.Requires(node != null);
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index cf33e23e..d8707bc4 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -427,9 +427,9 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Cmd>() != null);
return (Cmd)this.Visit(node); // Call general visit so subtypes get visited by their particular visitor
}
- public virtual RESeq VisitRESeq(RESeq reSeq) {
+ public virtual List<RE> VisitRESeq(List<RE> reSeq) {
Contract.Requires(reSeq != null);
- Contract.Ensures(Contract.Result<RESeq>() != null);
+ Contract.Ensures(Contract.Result<List<RE>>() != null);
for (int i = 0, n = reSeq.Count; i < n; i++)
reSeq[i] = (RE)this.VisitRE(cce.NonNull(reSeq[i]));
return reSeq;
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index c6cf5221..6dc69528 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -794,9 +794,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false);
throw new cce.UnreachableException();
}
- public override RESeq VisitRESeq(RESeq reSeq) {
+ public override List<RE> VisitRESeq(List<RE> reSeq) {
//Contract.Requires(reSeq != null);
- Contract.Ensures(Contract.Result<RESeq>() != null);
+ Contract.Ensures(Contract.Result<List<RE>>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
|