diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 225 | ||||
| -rw-r--r-- | Source/Core/Util.cs | 9 |
2 files changed, 190 insertions, 44 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 4b4dfd9e..7622cbdf 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -95,13 +95,23 @@ namespace Microsoft.Boogie { [ContractClass(typeof(AbsyContracts))]
public abstract class Absy {
- public IToken/*!*/ tok;
+ private IToken/*!*/ _tok;
private int uniqueId;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(tok != null);
+ Contract.Invariant(this._tok != null);
}
+ public IToken tok { //Rename this property and "_tok" if possible
+ get {
+ Contract.Ensures(Contract.Result<IToken>() != null);
+ return this._tok;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._tok = value;
+ }
+ }
public int Line {
get {
@@ -116,7 +126,7 @@ namespace Microsoft.Boogie { public Absy(IToken tok) {
Contract.Requires(tok != null);
- this.tok = tok;
+ this._tok = tok;
this.uniqueId = AbsyNodeCount++;
}
@@ -310,7 +320,7 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));
+ Contract.Invariant(cce.NonNullElements(this.topLevelDeclarations));
Contract.Invariant(globalVariablesCache == null || cce.NonNullElements(globalVariablesCache));
}
@@ -468,17 +478,21 @@ namespace Microsoft.Boogie { {
get
{
- return topLevelDeclarations;
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Declaration>>()));
+ return topLevelDeclarations.AsReadOnly();
}
set
{
+ Contract.Requires(value != null);
// materialize the decls, in case there is any dependency
// back on topLevelDeclarations
var v = value.ToList();
+ // remove null elements
+ v.RemoveAll(d => (d == null));
// now clear the decls
ClearTopLevelDeclarations();
- // and add the value
+ // and add the values
AddTopLevelDeclarations(v);
}
}
@@ -486,6 +500,7 @@ namespace Microsoft.Boogie { public void AddTopLevelDeclaration(Declaration decl)
{
Contract.Requires(!TopLevelDeclarationsAreFrozen);
+ Contract.Requires(decl != null);
topLevelDeclarations.Add(decl);
this.globalVariablesCache = null;
@@ -494,6 +509,7 @@ namespace Microsoft.Boogie { public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)
{
Contract.Requires(!TopLevelDeclarationsAreFrozen);
+ Contract.Requires(cce.NonNullElements(decls));
topLevelDeclarations.AddRange(decls);
this.globalVariablesCache = null;
@@ -1445,10 +1461,22 @@ namespace Microsoft.Boogie { }
public class Axiom : Declaration {
- public Expr/*!*/ Expr;
+ private Expr/*!*/ expression;
+
+ public Expr Expr {
+ get {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ return this.expression;
+ }
+ set {
+ Contract.Requires(value != null);
+ this.expression = value;
+ }
+ }
+
[ContractInvariantMethod]
void ExprInvariant() {
- Contract.Invariant(Expr != null);
+ Contract.Invariant(this.expression != null);
}
public string Comment;
@@ -1463,7 +1491,7 @@ namespace Microsoft.Boogie { : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Expr = expr;
+ this.expression = expr;
Comment = comment;
}
@@ -1620,15 +1648,38 @@ namespace Microsoft.Boogie { }
public class TypeSynonymDecl : NamedDeclaration {
- public List<TypeVariable>/*!*/ TypeParameters;
- public Type/*!*/ Body;
+ private List<TypeVariable>/*!*/ typeParameters;
+
+ public List<TypeVariable> TypeParameters {
+ get {
+ Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
+ return this.typeParameters;
+ }
+ set {
+ Contract.Requires(value != null);
+ this.typeParameters = value;
+ }
+ }
+
+ private Type/*!*/ body;
+
+ public Type Body {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this.body;
+ }
+ set {
+ Contract.Requires(value != null);
+ this.body = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(TypeParameters != null);
- Contract.Invariant(Body != null);
+ Contract.Invariant(this.body != null);
+ Contract.Invariant(this.typeParameters != null);
}
-
public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name,
List<TypeVariable>/*!*/ typeParams, Type/*!*/ body)
: base(tok, name) {
@@ -1636,8 +1687,8 @@ namespace Microsoft.Boogie { Contract.Requires(name != null);
Contract.Requires(typeParams != null);
Contract.Requires(body != null);
- this.TypeParameters = typeParams;
- this.Body = body;
+ this.typeParameters = typeParams;
+ this.body = body;
}
public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name,
List<TypeVariable>/*!*/ typeParams, Type/*!*/ body, QKeyValue kv)
@@ -1646,8 +1697,8 @@ namespace Microsoft.Boogie { Contract.Requires(name != null);
Contract.Requires(typeParams != null);
Contract.Requires(body != null);
- this.TypeParameters = typeParams;
- this.Body = body;
+ this.typeParameters = typeParams;
+ this.body = body;
this.Attributes = kv;
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -1786,24 +1837,36 @@ namespace Microsoft.Boogie { }
public abstract class Variable : NamedDeclaration {
- public TypedIdent/*!*/ TypedIdent;
+ private TypedIdent/*!*/ typedIdent;
+
+ public TypedIdent TypedIdent {
+ get {
+ Contract.Ensures(Contract.Result<TypedIdent>() != null);
+ return this.typedIdent;
+ }
+ set {
+ Contract.Requires(value != null);
+ this.typedIdent = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(TypedIdent != null);
+ Contract.Invariant(this.typedIdent != null);
}
public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent)
: base(tok, typedIdent.Name) {
Contract.Requires(tok != null);
Contract.Requires(typedIdent != null);
- this.TypedIdent = typedIdent;
+ this.typedIdent = typedIdent;
}
public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv)
: base(tok, typedIdent.Name) {
Contract.Requires(tok != null);
Contract.Requires(typedIdent != null);
- this.TypedIdent = typedIdent;
+ this.typedIdent = typedIdent;
this.Attributes = kv;
}
@@ -2692,11 +2755,24 @@ namespace Microsoft.Boogie { public class Requires : Absy, IPotentialErrorNode {
public readonly bool Free;
- public Expr/*!*/ Condition;
+
+ private Expr/*!*/ _condition;
+
+ public Expr/*!*/ Condition {
+ get {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ return this._condition;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._condition = value;
+ }
+ }
+
public string Comment;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Condition != null);
+ Contract.Invariant(this._condition != null);
Contract.Invariant(errorData == null || errorData is string);
}
@@ -2736,7 +2812,7 @@ namespace Microsoft.Boogie { Contract.Requires(condition != null);
Contract.Requires(token != null);
this.Free = free;
- this.Condition = condition;
+ this._condition = condition;
this.Comment = comment;
this.Attributes = kv;
}
@@ -3908,12 +3984,37 @@ namespace Microsoft.Boogie { public class TypedIdent : Absy {
public const string NoName = "";
- public string/*!*/ Name;
- public Type/*!*/ Type;
+
+ private string/*!*/ _name;
+
+ public string/*!*/ Name {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return this._name;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._name = value;
+ }
+ }
+
+ private Type/*!*/ _type;
+
+ public Type/*!*/ Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this._type;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._type = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Name != null);
- Contract.Invariant(Type != null);
+ Contract.Invariant(this._name != null);
+ Contract.Invariant(this._type != null);
}
public Expr WhereExpr;
@@ -3933,8 +4034,8 @@ namespace Microsoft.Boogie { Contract.Requires(name != null);
Contract.Requires(type != null);
Contract.Ensures(this.WhereExpr == whereExpr);
- this.Name = name;
- this.Type = type;
+ this._name = name;
+ this._type = type;
this.WhereExpr = whereExpr;
}
public bool HasName {
@@ -4151,20 +4252,45 @@ namespace Microsoft.Boogie { }
}
public class Sequential : CompoundRE {
- public RE/*!*/ first;
- public RE/*!*/ second;
+ private RE/*!*/ _first;
+
+ public RE/*!*/ first {
+ get {
+ Contract.Ensures(Contract.Result<RE>() != null);
+ return this._first;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._first = value;
+ }
+ }
+
+ private RE/*!*/ _second;
+
+ public RE/*!*/ second {
+ get {
+ Contract.Ensures(Contract.Result<RE>() != null);
+ return this._second;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._second = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(first != null);
- Contract.Invariant(second != null);
+ Contract.Invariant(this._first != null);
+ Contract.Invariant(this._second != null);
}
- public Sequential(RE a, RE b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- first = a;
- second = b;
+ public Sequential(RE first, RE second) {
+ Contract.Requires(first != null);
+ Contract.Requires(second != null);
+ this._first = first;
+ this._second = second;
}
+
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
stream.WriteLine();
@@ -4182,14 +4308,27 @@ namespace Microsoft.Boogie { public class Choice : CompoundRE {
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(rs != null);
+ Contract.Invariant(this._rs != null);
+ }
+
+ private List<RE>/*!*/ _rs;
+
+ public List<RE>/*!*/ rs { //Rename this (and _rs) if possible
+ get {
+ Contract.Ensures(Contract.Result<List<RE>>() != null);
+ return this._rs;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._rs = value;
+ }
}
- public List<RE>/*!*/ rs;
public Choice(List<RE> operands) {
Contract.Requires(operands != null);
- rs = operands;
+ this._rs = operands;
}
+
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
stream.WriteLine();
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 06e4fcf0..b28ac042 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -226,7 +226,14 @@ namespace Microsoft.Boogie { public void SetToken(Absy absy) {
Contract.Requires(absy != null);
- this.SetToken(ref absy.tok);
+ this.SetToken(t => absy.tok = t);
+ }
+
+ public void SetToken(Action<IToken> setter) {
+ Contract.Requires(setter != null);
+ if (this.setTokens) {
+ setter(this.CurrentToken);
+ }
}
public void SetToken(ref IToken tok) {
|