diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-05 12:49:13 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-05 12:49:13 -0800 |
| commit | dc96968bfaab78995a6a54e6960a942b804dfe18 (patch) | |
| tree | 12ba0bb1e8da12d23fcc2d932f029772a18e4254 /Source/Houdini | |
| parent | 4266ee07457dfacdee4f037f4907b4db1758bfec (diff) | |
further fixes to houdini
Diffstat (limited to 'Source/Houdini')
| -rw-r--r-- | Source/Houdini/Houdini.cs | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 986bc80c..f6dd07bf 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -308,25 +308,30 @@ namespace Microsoft.Boogie.Houdini { impl.OriginalLocVars = impl.LocVars;
}
foreach (Implementation impl in callGraph.Nodes) {
+ CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
+ CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
Inliner.ProcessImplementationForHoudini(program, impl);
+ CommandLineOptions.Clo.ProcedureInlining = savedOption;
}
foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
}
- int count = CommandLineOptions.Clo.InlineDepth;
Graph<Implementation> oldCallGraph = callGraph;
+ callGraph = new Graph<Implementation>();
+ foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) {
+ callGraph.AddEdge(edge.Item1, edge.Item2);
+ }
+ int count = CommandLineOptions.Clo.InlineDepth;
while (count > 0) {
- callGraph = new Graph<Implementation>();
- foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) {
- callGraph.AddEdge(edge.Item1, edge.Item2);
- }
foreach (Implementation impl in oldCallGraph.Nodes) {
- foreach (Implementation succ0 in oldCallGraph.Successors(impl)) {
- foreach (Implementation succ1 in oldCallGraph.Successors(succ0)) {
- callGraph.AddEdge(impl, succ1);
- }
+ List<Implementation> newNodes = new List<Implementation>();
+ foreach (Implementation succ in callGraph.Successors(impl)) {
+ newNodes.AddRange(oldCallGraph.Successors(succ));
+ }
+ foreach (Implementation newNode in newNodes) {
+ callGraph.AddEdge(impl, newNode);
}
}
count--;
|