diff options
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 24 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 4 |
2 files changed, 12 insertions, 16 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index ed079a58..ae9a56d4 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1283,14 +1283,12 @@ namespace Microsoft.Boogie { }
}
- internal IList<AssignLhs/*!*/>/*!*/ Lhss_NRO
+ internal void SetLhs(int index, AssignLhs lhs)
{
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IList<AssignLhs>>()));
- Contract.Ensures(!Contract.Result<IList<AssignLhs>>().IsReadOnly);
- return this._lhss;
- }
+ Contract.Requires(0 <= index && index < this.Lhss.Count);
+ Contract.Requires(lhs != null);
+ Contract.Ensures(this.Lhss[index] == lhs);
+ this._lhss[index] = lhs;
} private List<Expr/*!*/>/*!*/ _rhss;
@@ -1307,14 +1305,12 @@ namespace Microsoft.Boogie { }
}
- internal IList<Expr/*!*/>/*!*/ Rhss_NRO
+ internal void SetRhs(int index, Expr rhs)
{
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IList<Expr>>()));
- Contract.Ensures(!Contract.Result<IList<Expr>>().IsReadOnly);
- return this._rhss;
- }
+ Contract.Requires(0 <= index && index < this.Rhss.Count);
+ Contract.Requires(rhs != null);
+ Contract.Ensures(this.Rhss[index] == rhs);
+ this._rhss[index] = rhs;
}
[ContractInvariantMethod]
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 0284549b..98ea4df3 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -75,8 +75,8 @@ namespace Microsoft.Boogie { Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
for (int i = 0; i < node.Lhss.Count; ++i) {
- node.Lhss_NRO[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));
- node.Rhss_NRO[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));
+ node.SetLhs(i, cce.NonNull((AssignLhs)this.Visit(node.Lhss[i])));
+ node.SetRhs(i, cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i])));
}
return node;
}
|