diff options
| author |  qadeer <unknown> | 2010-04-17 19:14:43 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-04-17 19:14:43 +0000 |
| commit | d03242f9efa515d848f9166244bfaaa9fefd22b0 (patch) | |
| tree | 67c010e1d67394aff7c66d652e4a17e7efddd99a /Source/BoogieDriver | |
| parent | 584e66329027e1ea3faff5253a0b5554d455df49 (diff) | |
First cut of lazy inlining. The option can be turned on by the flag /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.ssc | 21 |
1 files changed, 6 insertions, 15 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index f68a9bbe..286f1036 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -435,9 +435,11 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
bool inline = false;
foreach (Declaration d in TopLevelDeclarations) {
- if (d.FindExprAttribute("inline") != null) inline = true;
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
}
- if (inline) {
+ if (inline && !CommandLineOptions.Clo.LazyInlining) {
foreach (Declaration d in TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null) {
@@ -517,7 +519,7 @@ namespace Microsoft.Boogie vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
} else
{
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
}
}
catch (ProverException e)
@@ -682,18 +684,7 @@ namespace Microsoft.Boogie }
if (CommandLineOptions.Clo.ErrorTrace > 0) {
Console.WriteLine("Execution trace:");
- foreach (Block! b in error.Trace) {
- if (b.tok == null) {
- Console.WriteLine(" <intermediate block>");
- } else {
- // for ErrorTrace == 1 restrict the output;
- // do not print tokens with -17:-4 as their location because they have been
- // introduced in the translation and do not give any useful feedback to the user
- if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {
- Console.WriteLine(" {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);
- }
- }
- }
+ error.Print(4);
}
errorCount++;
}
|