diff options
| -rw-r--r-- | Source/Core/Absy.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 |
2 files changed, 4 insertions, 0 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 0c9538d4..32b27ae6 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2112,6 +2112,7 @@ namespace Microsoft.Boogie { stream.WriteLine(this, level, "// " + Comment);
}
stream.Write(this, level, "{0}ensures ", Free ? "free " : "");
+ Cmd.EmitAttributes(stream, Attributes);
this.Condition.Emit(stream);
stream.WriteLine(";");
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 2f7f120d..0bcbad35 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -25,6 +25,7 @@ namespace VC private Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
public bool PersistCallTree;
public static Dictionary<string, int> callTree = null;
+ public int numInlined = 0;
public readonly static string recordProcName = "boogie_si_record";
[ContractInvariantMethod]
@@ -1576,6 +1577,8 @@ namespace VC #endregion
coverageManager.stop();
+ numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);
+
// Store current call tree
if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound))
{
|