diff options
| author |  tabarbe <unknown> | 2010-07-16 22:44:33 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-16 22:44:33 +0000 |
| commit | f6f281a60449aea24b257b73cd45fd970afbc57c (patch) | |
| tree | 879f030745bf494e95624aa2878039fe5ca0dd37 /Source/AbsInt/LoopInvariantsOnDemand.cs | |
| parent | 951ae331104cd20be6241b009ead77bef850fdb9 (diff) | |
Boogie: I have successfully ported the AbsInt project. It passes all regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL.
Address any error complaints to t-abarbe@microsoft.com
Diffstat (limited to 'Source/AbsInt/LoopInvariantsOnDemand.cs')
| -rw-r--r-- | Source/AbsInt/LoopInvariantsOnDemand.cs | 94 |
1 files changed, 49 insertions, 45 deletions
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs index 1ebd11b2..49958289 100644 --- a/Source/AbsInt/LoopInvariantsOnDemand.cs +++ b/Source/AbsInt/LoopInvariantsOnDemand.cs @@ -3,76 +3,80 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-namespace Microsoft.Boogie.AbstractInterpretation
-{
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using Microsoft.Contracts;
-using AI = Microsoft.AbstractInterpretationFramework;
-using Boogie = Microsoft.Boogie;
+namespace Microsoft.Boogie.AbstractInterpretation {
+ using System;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics.Contracts;
+ using AI = Microsoft.AbstractInterpretationFramework;
+ using Boogie = Microsoft.Boogie;
+
+
+
/// <summary>
/// A visitor of an abstract interpretation expression that collects the free variables
/// </summary>
- class FreeVariablesVisitor : AI.ExprVisitor
- {
- [Peer] List<AI.IVariable!>! variables;
- public List<AI.IVariable!>! FreeVariables
- {
- get
- {
+ class FreeVariablesVisitor : AI.ExprVisitor {
+ [Peer]
+ List<AI.IVariable> variables;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(variables));
+ Contract.Invariant(cce.NonNullElements(varNames));
+ }
+
+ public List<AI.IVariable> FreeVariables {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<AI.IVariable>>()));
+
return this.variables;
- }
+ }
}
- List<string!>! varNames; // used to check the consinstency!
+ List<string> varNames; // used to check the consinstency!
- public FreeVariablesVisitor()
- {
- this.variables = new List<AI.IVariable!>();
- this.varNames = new List<string!>();
+ public FreeVariablesVisitor() {
+ this.variables = new List<AI.IVariable>();
+ this.varNames = new List<string>();
}
- override public object Default(AI.IExpr! expr)
- {
- if (expr is AI.IVariable)
- {
- if(!variables.Contains((AI.IVariable) expr))
- {
- this.variables.Add((AI.IVariable) expr);
-
- assert ! this.varNames.Contains(expr.ToString()); // If we get there, we have an error: two variables with the same name but different identity
-
+ override public object Default(AI.IExpr expr) {
+ Contract.Requires(expr != null);
+ if (expr is AI.IVariable) {
+ if (!variables.Contains((AI.IVariable)expr)) {
+ this.variables.Add((AI.IVariable)expr);
+
+ Contract.Assert(!this.varNames.Contains(expr.ToString())); // If we get there, we have an error: two variables with the same name but different identity
+
this.varNames.Add(expr.ToString());
}
return null;
- }
- else if (expr is AI.IFunApp)
- return VisitFunApp((AI.IFunApp) expr);
+ } else if (expr is AI.IFunApp)
+ return VisitFunApp((AI.IFunApp)expr);
else if (expr is AI.IFunction)
return VisitFunction((AI.IFunction)expr);
- else
- {
- assert false;
+ else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
}
}
- public override object VisitFunApp(AI.IFunApp! funapp)
- {
- foreach (AI.IExpr! arg in funapp.Arguments)
- {
+ public override object VisitFunApp(AI.IFunApp funapp) {
+ Contract.Requires(funapp != null);
+ foreach (AI.IExpr arg in funapp.Arguments) {
+ Contract.Assert(arg != null);
arg.DoVisit(this);
}
return true;
}
-
- public override object VisitFunction(AI.IFunction! fun)
- {
+
+ public override object VisitFunction(AI.IFunction fun) {
+ Contract.Requires(fun != null);
fun.Body.DoVisit(this);
this.variables.Remove(fun.Param);
return true;
}
- }
+ }
}
\ No newline at end of file |