further fixes

2 files changed, 36 insertions, 10 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 56104eb7..4db83be0 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -20,6 +20,7 @@ namespace Microsoft.Boogie {
   public class CalleeCounterexampleInfo {

     public Counterexample counterexample;

     public List<Model.Element>/*!>!*/ args;

+    public int stateIndex;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -28,6 +29,14 @@ namespace Microsoft.Boogie {
     }

 

 

+    public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x, int i) {

+      Contract.Requires(cex != null);

+      Contract.Requires(cce.NonNullElements(x));

+      counterexample = cex;

+      args = x;

+      stateIndex = i;

+    }

+

     public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {

       Contract.Requires(cex != null);

       Contract.Requires(cce.NonNullElements(x));

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fec9258c..3ef44297 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2945,7 +2945,7 @@ namespace VC
               }

 

               int lastCandidate = 0;

-              int lastCapturePoint = 0;

+              int lastCapturePoint = CALL;

               for (int i = 0; i < this.orderedStateIds.Count; ++i) {

                 var s = orderedStateIds[i];

                 int candidate = s.Item1;

@@ -2958,22 +2958,35 @@ namespace VC
                   foreach (Variable v in info.AllVariables) {

                     init.AddBinding(v.Name, GetModelValue(m, v, candidate));

                   }

+                  lastCandidate = candidate;

+                  lastCapturePoint = capturePoint;

                   continue;

                 }

+

                 if (capturePoint == RETURN) {

+                  lastCandidate = candidate;

+                  lastCapturePoint = capturePoint;

                   continue;

                 }

 

                 Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);

                 VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];

-                var prevInc = (i > 0 && candidate == lastCandidate) ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

+                var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate) 

+                  ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

                 var cs = m.MkState(map.Description);

 

                 foreach (Variable v in info.AllVariables) {

                   var e = (Expr)map.IncarnationMap[v];

-                  if (e == null) continue;

 

-                  if (prevInc[v] == e) continue; // skip unchanged variables

+                  if (e == null) {

+                    if (lastCapturePoint == RETURN) {

+                      Contract.Assert(lastCandidate == candidate);

+                      cs.AddBinding(v.Name, GetModelValue(m, v, candidate));

+                    }

+                    continue;

+                  }

+

+                  if (lastCapturePoint != RETURN && prevInc[v] == e) continue; // skip unchanged variables

 

                   Model.Element elt;

                   if (e is IdentifierExpr) {

@@ -2990,6 +3003,7 @@ namespace VC
                   }

                   cs.AddBinding(v.Name, elt);

                 }

+

                 lastCandidate = candidate;

                 lastCapturePoint = capturePoint;

               }

@@ -3206,8 +3220,9 @@ namespace VC
                             calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                                 new CalleeCounterexampleInfo(

                                     cce.NonNull(GenerateTrace(labels, errModel, mvInfo, actualId, orderedStateIds, implName2StratifiedInliningInfo[calleeName].impl)),

-                                    new List<Model.Element>());

-                            orderedStateIds.Add(new Tuple<int, int>(actualId, StratifiedInliningErrorReporter.RETURN));

+                                    new List<Model.Element>(),

+                                    orderedStateIds.Count - 1);

+                            orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));

                         }

                         else

                         {

@@ -3224,8 +3239,9 @@ namespace VC
                                 calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                                     new CalleeCounterexampleInfo(

                                         cce.NonNull(GenerateTrace(labels, errModel, mvInfo, actualId, orderedStateIds, implName2StratifiedInliningInfo[calleeName].impl)),

-                                        new List<Model.Element>());

-                                orderedStateIds.Add(new Tuple<int, int>(actualId, StratifiedInliningErrorReporter.RETURN));

+                                        new List<Model.Element>(),

+                                        orderedStateIds.Count - 1);

+                                orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));

                               }

                               else {

                                 candidatesToExpand.Add(calleeId);

@@ -3236,8 +3252,9 @@ namespace VC
                               calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                                   new CalleeCounterexampleInfo(

                                       cce.NonNull(GenerateTrace(labels, errModel, mvInfo, calleeId, orderedStateIds, implName2StratifiedInliningInfo[calleeName].impl)),

-                                      new List<Model.Element>());

-                              orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.RETURN));

+                                      new List<Model.Element>(),

+                                      orderedStateIds.Count - 1);

+                              orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));

                             }

                         }

                     }