Bug fix in stratified inlining (triggered by {:inline} functions)

1 files changed, 6 insertions, 2 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];

           }

         }