diff options
| -rw-r--r-- | Source/Houdini/Houdini.cs | 27 | ||||
| -rw-r--r-- | Test/alltests.txt | 2 |
2 files changed, 19 insertions, 10 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 79c6fb77..7113293b 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -264,15 +264,8 @@ namespace Microsoft.Boogie.Houdini { }
private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions() {
- HashSet<Implementation> impls = new HashSet<Implementation>();
Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();
- foreach (Declaration decl in program.TopLevelDeclarations) {
- Implementation impl = decl as Implementation;
- if (impl != null && !impl.SkipVerification) {
- impls.Add(impl);
- }
- }
- foreach (Implementation impl in impls) {
+ foreach (Implementation impl in callGraph.Nodes) {
// make a different simplify log file for each function
String simplifyLog = null;
if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
@@ -328,8 +321,23 @@ namespace Microsoft.Boogie.Houdini { }
return callGraph;
}
-
+
private Queue<Implementation> BuildWorkList(Program program) {
+ // adding implementations to the workqueue from the bottom of the call graph upwards
+ Queue<Implementation> queue = new Queue<Implementation>();
+ StronglyConnectedComponents<Implementation> sccs =
+ new StronglyConnectedComponents<Implementation>(callGraph.Nodes,
+ new Adjacency<Implementation>(callGraph.Predecessors),
+ new Adjacency<Implementation>(callGraph.Successors));
+ sccs.Compute();
+ foreach (SCC<Implementation> scc in sccs) {
+ foreach (Implementation impl in scc) {
+ queue.Enqueue(impl);
+ }
+ }
+ return queue;
+
+ /*
Queue<Implementation> queue = new Queue<Implementation>();
foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
@@ -337,6 +345,7 @@ namespace Microsoft.Boogie.Houdini { queue.Enqueue(impl);
}
return queue;
+ */
}
private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
diff --git a/Test/alltests.txt b/Test/alltests.txt index 6e0073f2..e046dd06 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -20,7 +20,7 @@ codeexpr Use Tests code expressions prover Use Tests checking various prover options
test17 Postponed Tests inference of parameterized contracts
z3api Postponed Test for Z3 Managed .NET API prover
-houdini Postponed Test for Houdini decision procedure
+houdini Use Test for Houdini decision procedure
dafny0 Use Dafny functionality tests
dafny1 Use Various Dafny examples
dafny2 Use More Dafny examples
|