diff options
| author |  0biha <unknown> | 2014-12-19 13:05:19 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2014-12-19 13:05:19 +0100 |
| commit | fe2bc442dc600f540930f8a119722ca80f7da8e3 (patch) | |
| tree | e13648fbf5784cf5f7cee7628585e3b155e9abcf /Source/Core | |
| parent | d79ab18b7b02634e78b7b189387f231a9ff311db (diff) | |
Made 2 invariants of type 'StateCmd' robust by changing the design
(replaced public fields by private fields + getters/setters).
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 35 |
1 files changed, 29 insertions, 6 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 2c00bd8b..3f675317 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1724,20 +1724,43 @@ namespace Microsoft.Boogie { public class StateCmd : Cmd {
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Locals != null);
- Contract.Invariant(Cmds != null);
+ Contract.Invariant(this._locals != null);
+ Contract.Invariant(this._cmds != null);
+ }
+
+ private List<Variable> _locals;
+
+ public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals {
+ get {
+ Contract.Ensures(Contract.Result<List<Variable>>() != null);
+ return this._locals;
+ }
+ internal set {
+ Contract.Requires(value != null);
+ this._locals = value;
+ }
}
- public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals;
- public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds;
+ private List<Cmd> _cmds;
+
+ public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds {
+ get {
+ Contract.Ensures(Contract.Result<List<Variable>>() != null);
+ return this._cmds;
+ }
+ internal set {
+ Contract.Requires(value != null);
+ this._cmds = value;
+ }
+ }
public StateCmd(IToken tok, List<Variable>/*!*/ locals, List<Cmd>/*!*/ cmds)
: base(tok) {
Contract.Requires(locals != null);
Contract.Requires(cmds != null);
Contract.Requires(tok != null);
- this.Locals = locals;
- this.Cmds = cmds;
+ this._locals = locals;
+ this._cmds = cmds;
}
public override void Resolve(ResolutionContext rc) {
|