diff options
| author |  akashlal <unknown> | 2011-11-20 22:44:42 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2011-11-20 22:44:42 +0530 |
| commit | 50ebdd01228234e2311b61e59972519af3d512dc (patch) | |
| tree | e584e8cdced94911189123d4b79878fe8f0102e7 /Source/VCGeneration/Wlp.cs | |
| parent | 924a89f9022f0d4fa7201376eff55c0294cd4a72 (diff) | |
Added lazy summary computation to stratified inlining (not finished yet)
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index f5469ebf..c3134c09 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -149,6 +149,12 @@ namespace VC { AssumeCmd ac = (AssumeCmd)cmd;
if(CommandLineOptions.Clo.StratifiedInlining > 0) {
+ var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");
+ if(pname != null)
+ {
+ return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+ }
+
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {
|