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/Core | |
| 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/Core')
| -rw-r--r-- | Source/Core/Absy.ssc | 14 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.ssc | 1 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 24 |
3 files changed, 36 insertions, 3 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index d6d7bbc5..e83ca683 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -309,6 +309,18 @@ namespace Microsoft.Boogie {
return visitor.VisitProgram(this);
}
+
+ private List<GlobalVariable!> globals = null;
+ public List<GlobalVariable!>! GlobalVariables()
+ {
+ if (globals != null) return globals;
+ globals = new List<GlobalVariable!>();
+ foreach (Declaration d in TopLevelDeclarations) {
+ GlobalVariable gvar = d as GlobalVariable;
+ if (gvar != null) globals.Add(gvar);
+ }
+ return globals;
+ }
}
//---------------------------------------------------------------------
@@ -1516,7 +1528,7 @@ namespace Microsoft.Boogie this.Summary = new ProcedureSummary();
this.Attributes = kv;
}
-
+
public override void Emit(TokenTextWriter! stream, int level)
{
stream.Write(this, level, "procedure ");
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index eaf4e640..ab834cb2 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -1394,6 +1394,7 @@ namespace Microsoft.Boogie private IdentifierExpr! name;
public Function Func;
public FunctionCall(IdentifierExpr! name) { this.name = name; }
+ public FunctionCall(Function! f) { this.Func = f; this.name = new IdentifierExpr(Token.NoToken, f.Name); }
public string! FunctionName { get { return this.name.Name; } }
public AI.IFunctionSymbol! AIFunctionSymbol {
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 7b0bd6e0..e3b5293f 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -225,7 +225,8 @@ namespace Microsoft.Boogie public enum Inlining { None, Assert, Assume, Spec };
public Inlining ProcedureInlining = Inlining.Assume;
public bool PrintInlined = false;
-
+ public bool LazyInlining = false;
+
public enum TypeEncoding { None, Predicates, Arguments, Monomorphic };
public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates;
@@ -943,7 +944,20 @@ namespace Microsoft.Boogie }
}
break;
-
+ case "-lazyInline":
+ case "/lazyInline":
+ if (ps.ConfirmArgumentCount(1)) {
+ switch (args[ps.i])
+ {
+ case "0":
+ LazyInlining = false;
+ break;
+ case "1":
+ LazyInlining = true;
+ break;
+ }
+ }
+ break;
case "-typeEncoding":
case "/typeEncoding":
if (ps.ConfirmArgumentCount(1)) {
@@ -1287,6 +1301,12 @@ namespace Microsoft.Boogie if (UseArrayTheory) {
Monomorphize = true;
}
+
+ if (LazyInlining) {
+ PrintErrorModel = 1;
+ TypeEncodingMethod = TypeEncoding.Monomorphic;
+ UseArrayTheory = true;
+ }
}
|