diff options
| author |  akashlal <unknown> | 2013-10-21 19:47:24 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-10-21 19:47:24 +0530 |
| commit | 350ccedd0c5e4816d03ab2c2231ba8012557da74 (patch) | |
| tree | 3ec09959822e601de9bd31ad338a87250ccae0c4 | |
| parent | 17bf21691f93d99f63d56a85a5fa3b788a93828c (diff) | |
Bug fix in stratified inlining (triggered by {:inline} functions)
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 2 |
2 files changed, 7 insertions, 3 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 086dde15..ce0eb0a0 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2178,9 +2178,10 @@ namespace VC { string calleeName = naryExpr.Fun.FunctionName;
VCExprNAry callExpr = retnary[0] as VCExprNAry;
- Contract.Assert(callExpr != null);
+
if (implName2StratifiedInliningInfo.ContainsKey(calleeName)) {
+ Contract.Assert(callExpr != null);
int candidateId = GetNewId(callExpr);
boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;
candidateParent[candidateId] = currInlineCount;
@@ -2193,13 +2194,16 @@ namespace VC { return Gen.LabelPos(label, id2ControlVar[candidateId]);
}
else if (calleeName.StartsWith(recordProcName)) {
+ Contract.Assert(callExpr != null);
Debug.Assert(callExpr.Length == 1);
Debug.Assert(callExpr[0] != null);
recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0];
return callExpr;
}
else {
- return callExpr;
+ // callExpr can be null; this happens when the FunctionCall was on a
+ // pure function (not procedure) and the function got inlined
+ return retnary[0];
}
}
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index bb2a2785..c9b7ae83 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -152,7 +152,7 @@ namespace VC { 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) {
|