diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-11-16 10:34:45 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-11-16 10:34:45 +0530 |
| commit | 7ae95fdc63d65bf9768f07a873d36f87842da0cf (patch) | |
| tree | a83b51d5ba24ad06f5066334b45591f08207763c /Source/VCGeneration | |
| parent | b13899eb71d162ca976bfcd6ed774a1c99717372 (diff) | |
Debugging output for stratified inlining. Emit attribute on Ensures while
printing it.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 |
1 files changed, 3 insertions, 0 deletions
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))
{
|