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.

1 files changed, 1 insertions, 0 deletions

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 {