diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 28 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 4 |
2 files changed, 26 insertions, 6 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index be712ffb..ed079a58 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1281,6 +1281,16 @@ namespace Microsoft.Boogie { Contract.Requires(cce.NonNullElements(value));
this._lhss = new List<AssignLhs>(value);
}
+ }
+
+ internal IList<AssignLhs/*!*/>/*!*/ Lhss_NRO
+ {
+ get
+ {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IList<AssignLhs>>()));
+ Contract.Ensures(!Contract.Result<IList<AssignLhs>>().IsReadOnly);
+ return this._lhss;
+ }
} private List<Expr/*!*/>/*!*/ _rhss;
@@ -1297,6 +1307,16 @@ namespace Microsoft.Boogie { }
}
+ internal IList<Expr/*!*/>/*!*/ Rhss_NRO
+ {
+ get
+ {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IList<Expr>>()));
+ Contract.Ensures(!Contract.Result<IList<Expr>>().IsReadOnly);
+ return this._rhss;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(this._lhss));
@@ -1304,13 +1324,13 @@ namespace Microsoft.Boogie { }
- public AssignCmd(IToken tok, List<AssignLhs/*!*/>/*!*/ lhss, List<Expr/*!*/>/*!*/ rhss)
+ public AssignCmd(IToken tok, IList<AssignLhs/*!*/>/*!*/ lhss, IList<Expr/*!*/>/*!*/ rhss)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(rhss));
Contract.Requires(cce.NonNullElements(lhss));
- this._lhss = lhss;
- this._rhss = rhss;
+ this._lhss = new List<AssignLhs>(lhss);
+ this._rhss = new List<Expr>(rhss);
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -1748,7 +1768,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<List<Variable>>() != null);
return this._cmds;
}
- internal set {
+ set {
Contract.Requires(value != null);
this._cmds = value;
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 3f3ad5ae..0284549b 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[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));
- node.Rhss[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[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]));
}
return node;
}
|