diff options
author | 2013-07-22 22:30:46 +0100 | |
---|---|---|
committer | 2013-07-22 22:30:46 +0100 | |
commit | 793c0c0ded44401a1d6ef1bf494dd0a3d0b8dc43 (patch) | |
tree | 2187085433b50195a7e2783e27d0386187806378 /Source/Core | |
parent | 48731a5c9679efa8bcf7920c279108927a85f2f1 (diff) |
RESeq: farewell
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/Absy.cs | 16 | ||||
-rw-r--r-- | Source/Core/Duplicator.cs | 6 | ||||
-rw-r--r-- | Source/Core/StandardVisitor.cs | 4 |
3 files changed, 8 insertions, 18 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;
|