diff options
| author |  wuestholz <unknown> | 2014-09-23 11:32:04 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-09-23 11:32:04 +0200 |
| commit | fb226b8b4b9315a0ad2df1fcd1b4a7f12e118791 (patch) | |
| tree | 9245479972ed887b26b013ba4fb6c05862767846 /Source/AbsInt | |
| parent | 2031fb15596b2a114f7b3e0bb85ff838507051a0 (diff) | |
Did some refactoring.
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/NativeLattice.cs | 15 | ||||
| -rw-r--r-- | Source/AbsInt/Traverse.cs | 31 |
2 files changed, 19 insertions, 27 deletions
diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs index 8bb44385..30014643 100644 --- a/Source/AbsInt/NativeLattice.cs +++ b/Source/AbsInt/NativeLattice.cs @@ -120,8 +120,7 @@ namespace Microsoft.Boogie.AbstractInterpretation // procedures.
return program
- .TopLevelDeclarations
- .Where(d => d is Implementation).Select(i => (Implementation)i)
+ .Implementations
.GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc);
}
@@ -137,17 +136,13 @@ namespace Microsoft.Boogie.AbstractInterpretation // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain
var initialElement = lattice.Top;
Contract.Assert(initialElement != null);
- foreach (var decl in program.TopLevelDeclarations) {
- var ax = decl as Axiom;
- if (ax != null) {
- initialElement = lattice.Constrain(initialElement, ax.Expr);
- }
+ foreach (var ax in program.Axioms) {
+ initialElement = lattice.Constrain(initialElement, ax.Expr);
}
// analyze each procedure
- foreach (var decl in program.TopLevelDeclarations) {
- var proc = decl as Procedure;
- if (proc != null && procedureImplementations.ContainsKey(proc)) {
+ foreach (var proc in program.Procedures) {
+ if (procedureImplementations.ContainsKey(proc)) {
// analyze each implementation of the procedure
foreach (var impl in procedureImplementations[proc]) {
// add the precondition to the axioms
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs index 633ad86e..184a4071 100644 --- a/Source/AbsInt/Traverse.cs +++ b/Source/AbsInt/Traverse.cs @@ -24,25 +24,22 @@ namespace Microsoft.Boogie { Contract.Requires(program != null);
cce.BeginExpose(program);
- foreach (Declaration m in program.TopLevelDeclarations) {
- Implementation impl = m as Implementation;
- if (impl != null) {
- if (impl.Blocks != null && impl.Blocks.Count > 0) {
- Contract.Assume(cce.IsConsistent(impl));
- cce.BeginExpose(impl);
- Block start = impl.Blocks[0];
- Contract.Assume(start != null);
- Contract.Assume(cce.IsConsistent(start));
- Visit(start);
-
- // We reset the state...
- foreach (Block b in impl.Blocks) {
- cce.BeginExpose(b);
- b.TraversingStatus = Block.VisitState.ToVisit;
- cce.EndExpose();
- }
+ foreach (var impl in program.Implementations) {
+ if (impl.Blocks != null && impl.Blocks.Count > 0) {
+ Contract.Assume(cce.IsConsistent(impl));
+ cce.BeginExpose(impl);
+ Block start = impl.Blocks[0];
+ Contract.Assume(start != null);
+ Contract.Assume(cce.IsConsistent(start));
+ Visit(start);
+
+ // We reset the state...
+ foreach (Block b in impl.Blocks) {
+ cce.BeginExpose(b);
+ b.TraversingStatus = Block.VisitState.ToVisit;
cce.EndExpose();
}
+ cce.EndExpose();
}
}
cce.EndExpose();
|