From d03242f9efa515d848f9166244bfaaa9fefd22b0 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 17 Apr 2010 19:14:43 +0000
Subject: 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.

---
 Source/VCExpr/VCExprAST.ssc | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'Source/VCExpr/VCExprAST.ssc')

diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc
index e08e6138..2b5003a6 100644
--- a/Source/VCExpr/VCExprAST.ssc
+++ b/Source/VCExpr/VCExprAST.ssc
@@ -24,6 +24,24 @@ namespace Microsoft.Boogie
     public static readonly VCExpr! False = new VCExprLiteral (Type.Bool);
     public static readonly VCExpr! True  = new VCExprLiteral (Type.Bool);
 
+    private Function ControlFlowFunction = null;
+    public VCExpr! ControlFlowFunctionApplication(VCExpr! e1, VCExpr! e2)
+    {
+      if (ControlFlowFunction == null) {
+        Formal! first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
+        Formal! second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
+        VariableSeq! inputs = new VariableSeq();
+        inputs.Add(first);
+        inputs.Add(second);
+        Formal! returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);
+        ControlFlowFunction = new Function(Token.NoToken, "ControlFlow", inputs, returnVar);
+      }
+      List<VCExpr!> args = new List<VCExpr!>();
+      args.Add(e1);
+      args.Add(e2);
+      return Function(BoogieFunctionOp(ControlFlowFunction), args);
+    }
+    
     public VCExpr! Integer(BigNum x) {
       return new VCExprIntLit(x);
     }
-- 
cgit v1.2.3