diff options
author | 2010-04-17 19:14:43 +0000 | |
---|---|---|
committer | 2010-04-17 19:14:43 +0000 | |
commit | d03242f9efa515d848f9166244bfaaa9fefd22b0 (patch) | |
tree | 67c010e1d67394aff7c66d652e4a17e7efddd99a /Source/VCExpr/VCExprAST.ssc | |
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/VCExpr/VCExprAST.ssc')
-rw-r--r-- | Source/VCExpr/VCExprAST.ssc | 18 |
1 files changed, 18 insertions, 0 deletions
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);
}
|