diff options
| author |  qadeer <unknown> | 2010-02-09 22:04:43 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-02-09 22:04:43 +0000 |
| commit | 0001ad60f8a65026680d041fa23809f5acb357b0 (patch) | |
| tree | 2ed0a902bcd3160b869b883d7fb86e2e35bb32d6 /Source/Core/Absy.ssc | |
| parent | de43467788a59c64e27a6bd339b973398bf165a8 (diff) | |
1. Fixed bug in StandardVisitor.ssc
2. Hoisted the call to inlining into BoogieDriver.ssc
3. Implemented a simple dead variable elimination
4. Perform inlining only for those procedures whose verification is not skipped
Diffstat (limited to 'Source/Core/Absy.ssc')
| -rw-r--r-- | Source/Core/Absy.ssc | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index 0632d83f..18d29c73 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -260,28 +260,6 @@ namespace Microsoft.Boogie AxiomExpander expander = new AxiomExpander(this, tc);
expander.CollectExpansions();
-
- if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
- bool inline = false;
- foreach (Declaration d in TopLevelDeclarations) {
- if (d.FindExprAttribute("inline") != null) inline = true;
- }
- if (inline) {
- foreach (Declaration d in TopLevelDeclarations) {
- Implementation impl = d as Implementation;
- if (impl != null) {
- impl.OriginalBlocks = impl.Blocks;
- impl.OriginalLocVars = impl.LocVars;
- }
- }
- foreach (Declaration d in TopLevelDeclarations) {
- Implementation impl = d as Implementation;
- if (impl != null) {
- Inliner.ProcessImplementation(tc, this, impl);
- }
- }
- }
- }
}
public void ComputeStronglyConnectedComponents()
|