summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-02-18 01:58:27 +0000
committerGravatar rustanleino <unknown>2010-02-18 01:58:27 +0000
commit36bda629c0083590c5e4d17f06e769f822617033 (patch)
tree1591f3b47a97f4bd3cc0333b0a0dc8eeb40c20de
parent0549304b5beaf553ba3e5fa6550a6b8e43e31553 (diff)
* Added "deprecated" comment in help message about /interprocInfer switch. The functionality is currently broken.
* Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
-rw-r--r--Source/AIFramework/CommonFunctionSymbols.ssc19
-rw-r--r--Source/AIFramework/Expr.ssc20
-rw-r--r--Source/AIFramework/Functional.ssc4
-rw-r--r--Source/AIFramework/Lattice.ssc2
-rw-r--r--Source/AIFramework/MultiLattice.ssc5
-rw-r--r--Source/AIFramework/Mutable.ssc3
-rw-r--r--Source/AIFramework/Polyhedra/LinearConstraint.ssc4
-rw-r--r--Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc8
-rw-r--r--Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc10
-rw-r--r--Source/AIFramework/VariableMap/ConstantAbstraction.ssc2
-rw-r--r--Source/AIFramework/VariableMap/DynamicTypeLattice.ssc2
-rw-r--r--Source/AIFramework/VariableMap/Intervals.ssc10
-rw-r--r--Source/AIFramework/VariableMap/Nullness.ssc2
-rw-r--r--Source/AIFramework/VariableMap/VariableMapLattice.ssc19
-rw-r--r--Source/AbsInt/AbstractInterpretation.ssc242
-rw-r--r--Source/AbsInt/ExprFactories.ssc8
-rw-r--r--Source/Basetypes/Set.ssc4
-rw-r--r--Source/Core/Absy.ssc22
-rw-r--r--Source/Core/AbsyCmd.ssc2
-rw-r--r--Source/Core/CommandLineOptions.ssc3
-rw-r--r--Source/Core/GraphAlgorithms.ssc4
-rw-r--r--Source/Core/OOLongUtil.ssc2
-rw-r--r--Source/Core/PureCollections.ssc24
-rw-r--r--Source/Graph/Graph.ssc6
-rw-r--r--Source/VCExpr/VCExprASTVisitors.ssc1
25 files changed, 205 insertions, 223 deletions
diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc
index 4e38fbcb..f014e963 100644
--- a/Source/AIFramework/CommonFunctionSymbols.ssc
+++ b/Source/AIFramework/CommonFunctionSymbols.ssc
@@ -30,11 +30,10 @@ namespace Microsoft.AbstractInterpretationFramework
// base();
}
-// public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } }
- public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } }
+ public AIType! AIType { get { return typ; } }
[NoDefaultContract]
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return display;
@@ -65,7 +64,7 @@ namespace Microsoft.AbstractInterpretationFramework
return isym != null && isym.Value.Equals(this.Value);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
return Value.GetHashCode();
@@ -97,7 +96,7 @@ namespace Microsoft.AbstractInterpretationFramework
return isym != null && isym.Value == this.Value && isym.Bits == this.Bits;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
unchecked {
@@ -126,7 +125,7 @@ namespace Microsoft.AbstractInterpretationFramework
return dsym != null && dsym.Value == this.Value;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
return Value.GetHashCode();
@@ -155,7 +154,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
[NoDefaultContract]
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode()
{
return Value.GetHashCode();
@@ -898,19 +897,19 @@ namespace Microsoft.AbstractInterpretationFramework
/// <summary>
/// Returns true iff "t" denotes a type constant.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool IsTypeConstant(IExpr! t);
/// <summary>
/// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool IsTypeEqual(IExpr! t0, IExpr! t1);
/// <summary>
/// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool IsSubType(IExpr! t0, IExpr! t1);
/// <summary>
diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc
index 94dc4dc7..42621239 100644
--- a/Source/AIFramework/Expr.ssc
+++ b/Source/AIFramework/Expr.ssc
@@ -35,7 +35,7 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
/// <param name="visitor">The expression visitor.</param>
/// <returns>The result of the visit.</returns>
- [Pure][Reads(ReadsAttribute.Reads.Owned)] object DoVisit(ExprVisitor! visitor);
+ [Pure] object DoVisit(ExprVisitor! visitor);
// TODO: Type checking of the expressions.
}
@@ -57,10 +57,10 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
public interface IFunApp : IExpr
{
- IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
+ IFunctionSymbol! FunctionSymbol { get; }
IList/*<IExpr!>*/! Arguments
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] get
+ [Pure][Rep] get
ensures result.IsReadOnly;
;
}
@@ -82,9 +82,9 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
public interface IFunction : IExpr
{
- IVariable! Param { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
- AIType! ParamType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
- IExpr! Body { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }
+ IVariable! Param { get; }
+ AIType! ParamType { get; }
+ IExpr! Body { get; }
IFunction! CloneWithBody(IExpr! body);
}
@@ -307,7 +307,7 @@ namespace Microsoft.AbstractInterpretationFramework
/// </summary>
public interface IFunctionSymbol
{
- AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep][ResultNotNewlyAllocated]
+ AIType! AIType { [Rep][ResultNotNewlyAllocated]
get; }
}
@@ -354,7 +354,7 @@ namespace Microsoft.AbstractInterpretationFramework
public IList/*<AIType!>*/! Arguments
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep]
+ [Pure][Rep]
get
ensures result.IsReadOnly;
{
@@ -364,12 +364,12 @@ namespace Microsoft.AbstractInterpretationFramework
public int Arity
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return argTypes.Count; }
+ get { return argTypes.Count; }
}
public AIType! ReturnType
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return retType; }
+ get { return retType; }
}
/* TODO Do we have the invariant that two functions are equal iff they're the same object.
diff --git a/Source/AIFramework/Functional.ssc b/Source/AIFramework/Functional.ssc
index 4c4a5791..1413230e 100644
--- a/Source/AIFramework/Functional.ssc
+++ b/Source/AIFramework/Functional.ssc
@@ -28,7 +28,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
/// <returns>true if the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the key; otherwise, false.</returns>
/// <param name="key">The key to locate in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />. </param>
/// <filterpriority>2</filterpriority>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
bool Contains(object! key);
/// <summary>Returns an <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
@@ -106,7 +106,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
return new FunctionalHashtable(r);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Contains(object! key)
{
return h.Contains(key);
diff --git a/Source/AIFramework/Lattice.ssc b/Source/AIFramework/Lattice.ssc
index 2b606492..2ecc49f8 100644
--- a/Source/AIFramework/Lattice.ssc
+++ b/Source/AIFramework/Lattice.ssc
@@ -576,7 +576,7 @@ namespace Microsoft.AbstractInterpretationFramework
return lattice.ToString(e);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return string.Format(
diff --git a/Source/AIFramework/MultiLattice.ssc b/Source/AIFramework/MultiLattice.ssc
index b6b6ba5e..761f4c7e 100644
--- a/Source/AIFramework/MultiLattice.ssc
+++ b/Source/AIFramework/MultiLattice.ssc
@@ -48,7 +48,7 @@ namespace Microsoft.AbstractInterpretationFramework
return new Elt(this);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
// string s = "MultiLattice+Elt{";
@@ -83,7 +83,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override ICollection<IVariable!>! FreeVariables()
{
List<IVariable!>! list = new List<IVariable!>();
@@ -522,7 +522,6 @@ namespace Microsoft.AbstractInterpretationFramework
public object Current
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
get
{
return this.Entry;
diff --git a/Source/AIFramework/Mutable.ssc b/Source/AIFramework/Mutable.ssc
index 894359ef..36bb3647 100644
--- a/Source/AIFramework/Mutable.ssc
+++ b/Source/AIFramework/Mutable.ssc
@@ -18,10 +18,9 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
// Without it, the contract inheritance rules will complain since it
// has nowhere to attach the out-of-band contract it gets from
// ICollection.Count that it gets from IWorkList.
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
public override int Count { get { return base.Count; } }
- [Pure][Reads(ReadsAttribute.Reads.Owned)] public bool IsEmpty()
+ [Pure] public bool IsEmpty()
{
return Count == 0;
}
diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.ssc b/Source/AIFramework/Polyhedra/LinearConstraint.ssc
index 9ce1552b..087c3696 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraint.ssc
+++ b/Source/AIFramework/Polyhedra/LinearConstraint.ssc
@@ -36,7 +36,7 @@ namespace Microsoft.AbstractInterpretationFramework
Relation = rel;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string s = null;
@@ -501,7 +501,7 @@ namespace Microsoft.AbstractInterpretationFramework
terms.Add(dimension, value);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string s = null;
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
index b4e33a28..a99a4ee8 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
@@ -172,7 +172,7 @@ namespace Microsoft.AbstractInterpretationFramework
return Constraints != null && Constraints.Count == 0;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
if (Constraints == null)
@@ -1055,12 +1055,12 @@ namespace Microsoft.AbstractInterpretationFramework
id = count;
count++;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "lambda" + id;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public object DoVisit(ExprVisitor! visitor)
{
return visitor.VisitVariable(this);
@@ -1697,7 +1697,7 @@ namespace Microsoft.AbstractInterpretationFramework
public TestVariable(string! name) {
this.name = name;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public object DoVisit(ExprVisitor! visitor) {
return visitor.VisitVariable(this);
}
diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc
index bcf9c64d..fdb8d86d 100644
--- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc
+++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc
@@ -43,7 +43,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return lcs.ToString();
@@ -54,7 +54,7 @@ namespace Microsoft.AbstractInterpretationFramework
lcs.Dump();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override ICollection<IVariable!>! FreeVariables()
{
return lcs.FreeVariables();
@@ -258,14 +258,14 @@ namespace Microsoft.AbstractInterpretationFramework
// base();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)] public object DoVisit(ExprVisitor! visitor) {
+ [Pure] public object DoVisit(ExprVisitor! visitor) {
return visitor.VisitFunApp(this);
}
- public IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return Prop.Not; } }
+ public IFunctionSymbol! FunctionSymbol { get { return Prop.Not; } }
public IList/*<IExpr!>*/! Arguments {
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get {
+ get {
IExpr[] args = new IExpr[] { arg };
return ArrayList.ReadOnly(args);
}
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
index 7b7fd87e..97fb57ce 100644
--- a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
+++ b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
@@ -31,7 +31,7 @@ namespace Microsoft.AbstractInterpretationFramework
public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc
index b9d1a7a4..8161cb3e 100644
--- a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc
+++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc
@@ -114,7 +114,7 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
diff --git a/Source/AIFramework/VariableMap/Intervals.ssc b/Source/AIFramework/VariableMap/Intervals.ssc
index 721b175d..7f6211ba 100644
--- a/Source/AIFramework/VariableMap/Intervals.ssc
+++ b/Source/AIFramework/VariableMap/Intervals.ssc
@@ -466,13 +466,13 @@ namespace Microsoft.AbstractInterpretationFramework
*/
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "[" + this.inf + ", " + this.sup + "]";
@@ -704,7 +704,7 @@ namespace Microsoft.AbstractInterpretationFramework
this.val = i;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return this.Value.ToString();
@@ -746,7 +746,7 @@ namespace Microsoft.AbstractInterpretationFramework
class PlusInfinity : InfinitaryInt
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "+oo";
@@ -768,7 +768,7 @@ namespace Microsoft.AbstractInterpretationFramework
class MinusInfinity : InfinitaryInt
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return "-oo";
diff --git a/Source/AIFramework/VariableMap/Nullness.ssc b/Source/AIFramework/VariableMap/Nullness.ssc
index 63d637ce..bbd1da70 100644
--- a/Source/AIFramework/VariableMap/Nullness.ssc
+++ b/Source/AIFramework/VariableMap/Nullness.ssc
@@ -27,7 +27,7 @@ namespace Microsoft.AbstractInterpretationFramework
public Elt (Value v) { this.value = v; }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
{
return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
index aa15f1e6..34f876f5 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
@@ -51,6 +51,22 @@ namespace Microsoft.AbstractInterpretationFramework
{
return new Elt(this.constraints);
}
+
+ [Pure]
+ public override string! ToString()
+ {
+ if (constraints == null) {
+ return "<bottom>";
+ }
+ string s = "[";
+ string sep = "";
+ foreach (IVariable! v in (!)constraints.Keys) {
+ Element m = (Element)constraints[v];
+ s += sep + v.Name + " -> " + m;
+ sep = ", ";
+ }
+ return s + "]";
+ }
public static Elt! Top = new Elt(true);
public static Elt! Bottom = new Elt(false);
@@ -61,7 +77,6 @@ namespace Microsoft.AbstractInterpretationFramework
}
public bool IsBottom {
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
get {
return this.constraints == null;
}
@@ -158,7 +173,7 @@ namespace Microsoft.AbstractInterpretationFramework
return new Elt(newMap);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override ICollection<IVariable!>! FreeVariables()
{
throw new System.NotImplementedException();
diff --git a/Source/AbsInt/AbstractInterpretation.ssc b/Source/AbsInt/AbstractInterpretation.ssc
index eee25a09..ee5a1f06 100644
--- a/Source/AbsInt/AbstractInterpretation.ssc
+++ b/Source/AbsInt/AbstractInterpretation.ssc
@@ -55,7 +55,6 @@ namespace Microsoft.Boogie.AbstractInterpretation
this.lattice = lattice;
this.procWorkItems = new Queue<ProcedureWorkItem!>();
this.callReturnWorkItems = new Queue();
- // base();
}
private Cci.IGraphNavigator ComputeCallGraph (Program! program)
@@ -198,17 +197,17 @@ namespace Microsoft.Boogie.AbstractInterpretation
// where the notation i' means a variable with the same (string) name as i,
// but a different identity.
- AI.Lattice.Element! releventToCall = knownAtCallSite;
+ AI.Lattice.Element! relevantToCall = knownAtCallSite;
for (int i=0; i<proc.InParams.Length; i++)
{
// "Assign" the actual expressions to the corresponding formal variables.
assume proc.InParams[i] != null; //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
assume call.Ins[i] != null; //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
Expr equality = Expr.Eq(Expr.Ident( (!) proc.InParams[i]), (!) call.Ins[i]);
- releventToCall = lattice.Constrain(releventToCall, equality.IExpr);
+ relevantToCall = lattice.Constrain(relevantToCall, equality.IExpr);
}
foreach (Variable! var in caller.LocVars) {
- releventToCall = this.lattice.Eliminate(releventToCall, var);
+ relevantToCall = this.lattice.Eliminate(relevantToCall, var);
}
ProcedureSummary! summary = proc.Summary;
@@ -218,7 +217,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
{
ProcedureSummaryEntry! current = (!) summary[i];
- if (lattice.Equivalent(current.OnEntry, releventToCall))
+ if (lattice.Equivalent(current.OnEntry, relevantToCall))
{
applicableEntry = current;
break;
@@ -228,7 +227,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
// Not found in current map, so add new entry.
if (applicableEntry == null)
{
- ProcedureWorkItem! newWorkItem = new ProcedureWorkItem(proc, releventToCall, lattice);
+ ProcedureWorkItem! newWorkItem = new ProcedureWorkItem(proc, relevantToCall, lattice);
this.procWorkItems.Enqueue(newWorkItem);
applicableEntry = (!) proc.Summary[newWorkItem.Index];
}
@@ -351,48 +350,8 @@ namespace Microsoft.Boogie.AbstractInterpretation
{
// process each procedure implementation by recursively processing the first (entry) block...
((!)impl.Blocks[0]).Lattice = lattice;
- ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry);
-
- if (!CommandLineOptions.Clo.IntraproceduralInfer)
- {
- // compute the procedure invariant by joining all terminal block invariants...
- AI.Lattice.Element post = lattice.Bottom;
- foreach (Block block in impl.Blocks)
- {
- if (block.TransferCmd is ReturnCmd)
- {
- // note: if program control cannot reach this block, then postValue will be null
- if (block.PostInvariant != null)
- {
- post = (AI.Lattice.Element) lattice.Join(post, block.PostInvariant);
- }
- }
- }
-
- AI.Lattice.Element atReturn = post;
- foreach (Variable! var in impl.LocVars)
- {
- atReturn = this.lattice.Eliminate(atReturn, var);
- }
- foreach (Variable! var in impl.InParams)
- {
- atReturn = this.lattice.Eliminate(atReturn, var);
- }
-
- if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))
- {
- // If the results of this analysis are strictly worse than
- // what we previous knew for the same input assumptions,
- // update the summary and re-do the call sites.
-
- summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);
-
- foreach (CallSite callSite in summaryEntry.ReturnPoints)
- {
- this.callReturnWorkItems.Enqueue(callSite);
- }
- }
- }
+ ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry, summaryEntry);
+ AdjustProcedureSummary(impl, summaryEntry);
}
}
}
@@ -402,13 +361,58 @@ namespace Microsoft.Boogie.AbstractInterpretation
{
CallSite callSite = (CallSite!) this.callReturnWorkItems.Dequeue();
- PropagateStartingAtStatement( callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall);
+ PropagateStartingAtStatement(callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall, callSite.SummaryEntry);
+ AdjustProcedureSummary(callSite.Impl, callSite.SummaryEntry);
}
-
} // both queues
}
+
+ void AdjustProcedureSummary(Implementation! impl, ProcedureSummaryEntry! summaryEntry)
+ {
+ if (CommandLineOptions.Clo.IntraproceduralInfer) {
+ return; // no summary to adjust
+ }
+
+ // compute the procedure invariant by joining all terminal block invariants...
+ AI.Lattice.Element post = lattice.Bottom;
+ foreach (Block block in impl.Blocks)
+ {
+ if (block.TransferCmd is ReturnCmd)
+ {
+ // note: if program control cannot reach this block, then postValue will be null
+ if (block.PostInvariant != null)
+ {
+ post = (AI.Lattice.Element) lattice.Join(post, block.PostInvariant);
+ }
+ }
+ }
+
+ AI.Lattice.Element atReturn = post;
+ foreach (Variable! var in impl.LocVars)
+ {
+ atReturn = this.lattice.Eliminate(atReturn, var);
+ }
+ foreach (Variable! var in impl.InParams)
+ {
+ atReturn = this.lattice.Eliminate(atReturn, var);
+ }
+
+ if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))
+ {
+ // If the results of this analysis are strictly worse than
+ // what we previous knew for the same input assumptions,
+ // update the summary and re-do the call sites.
+
+ summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);
+
+ foreach (CallSite! callSite in summaryEntry.ReturnPoints)
+ {
+ this.callReturnWorkItems.Enqueue(callSite);
+ }
+ }
+ }
private static int freshVarId = 0;
private static Variable! FreshVar(Boogie.Type! ty)
@@ -427,7 +431,8 @@ namespace Microsoft.Boogie.AbstractInterpretation
/// <param name="statementIndex"> </param>
/// <param name="currentValue"> The initial value </param>
/// </summary>
- private void PropagateStartingAtStatement (Implementation! impl, Block! block, int statementIndex, AI.Lattice.Element! currentValue)
+ private void PropagateStartingAtStatement (Implementation! impl, Block! block, int statementIndex, AI.Lattice.Element! currentValue,
+ ProcedureSummaryEntry! summaryEntry)
{
assume log.IsPeerConsistent;
log.DbgMsg(string.Format("{0}:", block.Label)); log.DbgMsgIndent();
@@ -439,7 +444,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
currentValue = Step(cmd, currentValue, impl, // Apply the transition function
delegate (AI.Lattice.Element! currentValue)
{
- return new CallSite(impl, block, cmdIndex, currentValue);
+ return new CallSite(impl, block, cmdIndex, currentValue, summaryEntry);
}
);
}
@@ -464,7 +469,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
{
succ.Lattice = block.Lattice; // The lattice is the same
// Propagate the post-abstract state of this block to the successor
- ComputeBlockInvariants(impl, succ, block.PostInvariant);
+ ComputeBlockInvariants(impl, succ, block.PostInvariant, summaryEntry);
}
}
}
@@ -680,8 +685,8 @@ namespace Microsoft.Boogie.AbstractInterpretation
/// <param name="block"> The block for which we compute the invariants </param>
/// <param name="incomingValue"> The "init" abstract state for the block </param>
/// </summary>
- private void ComputeBlockInvariants (Implementation! impl, Block! block, AI.Lattice.Element! incomingValue)
- {
+ private void ComputeBlockInvariants (Implementation! impl, Block! block, AI.Lattice.Element! incomingValue, ProcedureSummaryEntry! summaryEntry)
+ {
if (block.PreInvariant == null) // block has not yet been processed
{
assert block.PostInvariant == null;
@@ -709,7 +714,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
return;
}
#if DEBUG_PRINT
- // Compute the free variables in incoming and block.PreInvariant
+ // Compute the free variables in incoming and block.PreInvariant
FreeVariablesVisitor freeVarsVisitorForA = new FreeVariablesVisitor();
FreeVariablesVisitor freeVarsVisitorForB = new FreeVariablesVisitor();
@@ -766,47 +771,22 @@ namespace Microsoft.Boogie.AbstractInterpretation
#endif
#endregion
#region Propagate the entry abstract state through the method
- PropagateStartingAtStatement(impl, block, 0, (!) block.PreInvariant.Clone());
+ PropagateStartingAtStatement(impl, block, 0, (!) block.PreInvariant.Clone(), summaryEntry);
#endregion
}
#if DEBUG_PRINT
-private string! ToString(List<AI.IVariable!>! vars)
-{
- string s = "";
-
- foreach(AI.IVariable! v in vars)
- {
- s += v.Name +" ";
- }
- return s;
-}
-
-#endif
-
-
- /// <summary>
- /// Analyze the given set of blocks.
- /// <param name="blocks"> The set of blocks to analyze </param>
- /// <param name="entryPoint"> The initial block (from where we start the analysis </param>
- /// <param name="initialState"> The initial abstract state </param>
- /// </summary>
- public void AnalyzeBlocks(ICollection<Block!>! blocks, Block! entryPoint, AI.MathematicalLattice.Element! initialState)
- requires blocks.Contains(entryPoint);
+ private string! ToString(List<AI.IVariable!>! vars)
{
- TypeVariableSeq! dummyVarSeq = new TypeVariableSeq();
- VariableSeq! dummySeq = new VariableSeq();
- List<Block!> blockSequence = new List<Block!>();
-
- foreach(Block! block in blocks) {
- blockSequence.Add(block);
+ string s = "";
+
+ foreach(AI.IVariable! v in vars)
+ {
+ s += v.Name +" ";
}
-
- Implementation dummyImplementation =
- new Implementation(Token.NoToken, "dummyImplementation", dummyVarSeq, dummySeq, dummySeq, dummySeq, blockSequence);
-
- ComputeBlockInvariants(dummyImplementation, entryPoint, initialState);
+ return s;
}
+#endif
} // class
@@ -1004,58 +984,50 @@ private string! ToString(List<AI.IVariable!>! vars)
public class AbstractInterpretation
{
/// <summary>
- /// Run the abstract interpretation.
- /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn
- /// </summary>
- public static void RunAbstractInterpretation(Program! program)
- {
- Helpers.ExtraTraceInformation("Starting abstract interpretation");
-
- if(CommandLineOptions.Clo.UseAbstractInterpretation)
- {
- DateTime start = new DateTime(); // to please compiler's definite assignment rules
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine();
- Console.WriteLine("Running abstract interpretation...");
- start = DateTime.Now;
- }
-
- WidenPoints.Compute(program);
-
- if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)
- {
- AI.Lattice! lattice;
-
- lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;
-
- ApplyAbstractInterpretation(program, lattice);
+ /// Run the abstract interpretation.
+ /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn
+ /// </summary>
+ public static void RunAbstractInterpretation(Program! program)
+ {
+ Helpers.ExtraTraceInformation("Starting abstract interpretation");
- if (CommandLineOptions.Clo.Ai.DebugStatistics)
- {
- Console.Error.WriteLine(lattice);
- }
+ if(CommandLineOptions.Clo.UseAbstractInterpretation)
+ {
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine();
+ Console.WriteLine("Running abstract interpretation...");
+ start = DateTime.Now;
+ }
- if (!CommandLineOptions.Clo.IntraproceduralInfer)
- {
- Procedure.ShowSummaries = true;
- }
- }
- else // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)
- {
- AI.Lattice! lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;
- ApplyAbstractInterpretation(program, lattice);
- }
+ WidenPoints.Compute(program);
- program.InstrumentWithInvariants();
+ if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)
+ {
+ AI.Lattice lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;
+ ApplyAbstractInterpretation(program, lattice);
- if (CommandLineOptions.Clo.Trace) {
- DateTime end = DateTime.Now;
- TimeSpan elapsed = end - start;
- Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
- Console.Out.Flush();
+ if (CommandLineOptions.Clo.Ai.DebugStatistics)
+ {
+ Console.Error.WriteLine(lattice);
}
}
+ else // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)
+ {
+ AI.Lattice! lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;
+ ApplyAbstractInterpretation(program, lattice);
+ }
+
+ program.InstrumentWithInvariants();
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
+ Console.Out.Flush();
+ }
}
+ }
static void ApplyAbstractInterpretation (Program! program, AI.Lattice! lattice)
{
diff --git a/Source/AbsInt/ExprFactories.ssc b/Source/AbsInt/ExprFactories.ssc
index 1569c36c..ad090f2b 100644
--- a/Source/AbsInt/ExprFactories.ssc
+++ b/Source/AbsInt/ExprFactories.ssc
@@ -166,7 +166,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
/// <summary>
/// Returns true iff "t" denotes a type constant.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool IsTypeConstant(AI.IExpr! t)
ensures result == (t is Constant);
{
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
/// <summary>
/// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool IsTypeEqual(AI.IExpr! t0, AI.IExpr! t1) {
Constant c0 = t0 as Constant;
Constant c1 = t1 as Constant;
@@ -186,10 +186,9 @@ namespace Microsoft.Boogie.AbstractInterpretation {
/// <summary>
/// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
/// </summary>
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool IsSubType(AI.IExpr! t0, AI.IExpr! t1) {
assert false; // BUGBUG: TODO
- return false;
}
/// <summary>
@@ -198,7 +197,6 @@ namespace Microsoft.Boogie.AbstractInterpretation {
/// </summary>
public AI.IExpr! JoinTypes(AI.IExpr! t0, AI.IExpr! t1) {
assert false; // BUGBUG: TODO
- throw new System.NotImplementedException();
}
public AI.IFunApp! IsExactlyA(AI.IExpr! e, AI.IExpr! type) {
diff --git a/Source/Basetypes/Set.ssc b/Source/Basetypes/Set.ssc
index 221a9ad4..9286d6f5 100644
--- a/Source/Basetypes/Set.ssc
+++ b/Source/Basetypes/Set.ssc
@@ -189,7 +189,7 @@ namespace Microsoft.Boogie
public virtual int Count
{
- [Pure][Reads(ReadsAttribute.Reads.Owned)] get
+ get
{
return ht.Count;
}
@@ -201,7 +201,7 @@ namespace Microsoft.Boogie
return ht.Keys.GetEnumerator();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string s = null;
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index 18d29c73..35175881 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -15,17 +15,19 @@ namespace Microsoft.Boogie.AbstractInterpretation
public class CallSite
{
- public Implementation! Impl;
- public Block! Block;
- public int Statement; // invariant: Block[Statement] is CallCmd
- public AI.Lattice.Element! KnownBeforeCall;
+ public readonly Implementation! Impl;
+ public readonly Block! Block;
+ public readonly int Statement; // invariant: Block[Statement] is CallCmd
+ public readonly AI.Lattice.Element! KnownBeforeCall;
+ public readonly ProcedureSummaryEntry! SummaryEntry;
- public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e)
+ public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e, ProcedureSummaryEntry! summaryEntry)
{
this.Impl = impl;
this.Block = b;
this.Statement = stmt;
this.KnownBeforeCall = e;
+ this.SummaryEntry = summaryEntry;
}
}
@@ -532,7 +534,7 @@ namespace Microsoft.Boogie
this.name = name;
// base(tok);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return (!) Name;
@@ -775,7 +777,7 @@ namespace Microsoft.Boogie
TypecheckAttributes(tc);
this.TypedIdent.Typecheck(tc);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public object DoVisit(AI.ExprVisitor! visitor)
{
return visitor.VisitVariable(this);
@@ -1496,8 +1498,6 @@ namespace Microsoft.Boogie
[Rep]
public readonly ProcedureSummary! Summary;
- public static bool ShowSummaries = false;
-
public Procedure (
IToken! tok,
string! name,
@@ -1559,9 +1559,9 @@ namespace Microsoft.Boogie
e.Emit(stream, level);
}
- if (ShowSummaries)
+ if (!CommandLineOptions.Clo.IntraproceduralInfer)
{
- for (int s=0; s<this.Summary.Count; s++)
+ for (int s=0; s < this.Summary.Count; s++)
{
ProcedureSummaryEntry! entry = (!) this.Summary[s];
stream.Write(level + 1, "// ");
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index d0c65c96..da4f4247 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -775,7 +775,7 @@ namespace Microsoft.Boogie
this.PostInvariant = null;
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
return this.Label + (this.widenBlock? "[w]" : "");
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 2dd85a65..bed34c63 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -1842,7 +1842,8 @@ namespace Microsoft.Boogie
switch on its left
/checkInfer : instrument inferred invariants as asserts to be checked by
theorem prover
- /interprocInfer : perform interprocedural inference
+ /interprocInfer : perform interprocedural inference (deprecated, not
+ supported)
/contractInfer : perform procedure contract inference
/logInfer : print debug output during inference
/printInstrumented : print Boogie program after it has been
diff --git a/Source/Core/GraphAlgorithms.ssc b/Source/Core/GraphAlgorithms.ssc
index 7ce07d6e..aac45d73 100644
--- a/Source/Core/GraphAlgorithms.ssc
+++ b/Source/Core/GraphAlgorithms.ssc
@@ -33,7 +33,7 @@ namespace Microsoft.Boogie
public bool IsReadOnly { get { return nodesMap.IsReadOnly; } }
public void Add(Node item) { nodesMap.Add(item,null); }
public void Clear() { nodesMap.Clear(); }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Contains(Node item) { return nodesMap.ContainsKey(item); }
public void CopyTo(Node[]! array, int arrayIndex) { nodes.CopyTo(array, arrayIndex); }
public bool Remove(Node item) { return nodesMap.Remove(item); }
@@ -148,7 +148,7 @@ namespace Microsoft.Boogie
}
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString()
{
string outStr = "";
diff --git a/Source/Core/OOLongUtil.ssc b/Source/Core/OOLongUtil.ssc
index 81dadf1b..e87666f3 100644
--- a/Source/Core/OOLongUtil.ssc
+++ b/Source/Core/OOLongUtil.ssc
@@ -34,7 +34,7 @@ namespace Boogie.Util {
b.Flush();
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
return "<TeeWriter: " + a.ToString() + ", " + b.ToString() + ">";
}
diff --git a/Source/Core/PureCollections.ssc b/Source/Core/PureCollections.ssc
index d51ebe62..971af388 100644
--- a/Source/Core/PureCollections.ssc
+++ b/Source/Core/PureCollections.ssc
@@ -80,7 +80,7 @@ namespace PureCollections {
[Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
public static bool operator != (Tuple s, Tuple t) { return ! (t == s); }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode (){
int h =0;
assume this.elems != null;
@@ -120,7 +120,7 @@ namespace PureCollections {
}
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
assert this.elems != null;
if (elems.Length==0)
@@ -165,7 +165,7 @@ namespace PureCollections {
} while (index < map.elems.Length && map.elems[index] == null);
return index < map.elems.Length;
}
- public object Current{ [Pure][Reads(ReadsAttribute.Reads.Owned)] get {assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}
+ public object Current{ get { assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}
public void Reset() {index = -1; }
}
@@ -281,7 +281,7 @@ namespace PureCollections {
}
//ToString - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
if (card ==0)
return "{|->}";
@@ -351,7 +351,7 @@ namespace PureCollections {
public static bool operator != (Map s, Map t){
return ! (t == s);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode (){
int h =0;
assert this.elems != null;
@@ -368,7 +368,7 @@ namespace PureCollections {
//Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Has(Object x) {
if (x == null)
throw new MissingCase();
@@ -427,7 +427,7 @@ namespace PureCollections {
//while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);
return index < seq.Length;
}
- public object Current{ [Pure][Reads(ReadsAttribute.Reads.Owned)] get {assert seq.elems != null; return seq.elems[index]; }}
+ public object Current{ get { assert seq.elems != null; return seq.elems[index]; }}
public void Reset() {index = -1; }
}
@@ -546,7 +546,7 @@ namespace PureCollections {
}
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() {
string s ="";
assert this.elems != null;
@@ -596,7 +596,7 @@ namespace PureCollections {
public static bool operator != (Sequence s, Sequence t){
return !(s == t);
}
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override int GetHashCode (){
int h = 0;
for(int i = 0; i < card; i++)
@@ -645,7 +645,7 @@ namespace PureCollections {
public static bool operator >= (Sequence s, Sequence t){ return t <= s;}
//pure---------------------------------------------------------------
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public bool Has(object x) { // WS translate to tailrecursion
if (x == null)
throw new MissingCase();
@@ -658,7 +658,7 @@ namespace PureCollections {
// the index of the first occurrence of x in this sequence,
// or -1 if x does not occur
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public int IndexOf(object x) {
if (x == null)
throw new MissingCase();
@@ -671,7 +671,7 @@ namespace PureCollections {
// the index of the last occurrence of x in this sequence,
// or -1 if x does not occur
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public int LastIndexOf(object x) {
if (x == null)
throw new MissingCase();
diff --git a/Source/Graph/Graph.ssc b/Source/Graph/Graph.ssc
index c9795f15..dcbd12a3 100644
--- a/Source/Graph/Graph.ssc
+++ b/Source/Graph/Graph.ssc
@@ -91,7 +91,7 @@ internal class DomRelation<Node>{
return false;
}
private Dictionary<Node,List<Node>>? domMap = null;
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string ToString(){
assume this.doms != null;
int[] localDoms = this.doms;
@@ -269,7 +269,7 @@ public class Graph<Node> {
Node! myHeader;
internal PreHeader(Node! h) { myHeader = h; }
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() { return "#" + myHeader.ToString(); }
}
@@ -295,7 +295,7 @@ public class Graph<Node> {
{ es = new Set<Pair<Node!,Node!>>(); ns = new Set<Node>(); }
// BUGBUG: Set<T>.ToString() should return a non-null string
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ [Pure]
public override string! ToString() { return "" + es.ToString(); }
public void AddSource(Node! x)
diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc
index 47865747..2808f6bb 100644
--- a/Source/VCExpr/VCExprASTVisitors.ssc
+++ b/Source/VCExpr/VCExprASTVisitors.ssc
@@ -163,7 +163,6 @@ namespace Microsoft.Boogie.VCExprAST
}
public object Current {
- [Pure][Reads(ReadsAttribute.Reads.Owned)]
get {
return (!)CurrentExpr;
} }