diff options
author | schaef <unknown> | 2011-03-15 02:58:31 +0000 |
---|---|---|
committer | schaef <unknown> | 2011-03-15 02:58:31 +0000 |
commit | 3b95e484b2e097534bf150edc87bc1b19b5892bf (patch) | |
tree | f1ae58dc91efec7599a44d06908d85e83c9be2e4 /Source/VCGeneration/VC.cs | |
parent | b7829c73906c7ddbc01e7e076aa430f349ae9698 (diff) |
new algorithm for dead code detection (vc:doomed)
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r-- | Source/VCGeneration/VC.cs | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 8a9e13ff..f3517d60 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -20,7 +20,7 @@ namespace VC { using Bpl = Microsoft.Boogie;
public class VCGen : ConditionGeneration {
-
+ private const bool _print_time = false;
/// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
@@ -1587,10 +1587,17 @@ namespace VC { Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (impl.SkipVerification) {
return Outcome.Inconclusive; // not sure about this one
- }
-
- callback.OnProgress("VCgen", 0, 0, 0.0);
+ }
+ callback.OnProgress("VCgen", 0, 0, 0.0);
+
+ Stopwatch watch = new Stopwatch();
+ if (_print_time)
+ {
+ Console.WriteLine("Checking function {0}", impl.Name);
+ watch.Reset();
+ watch.Start();
+ }
ConvertCFG2DAG(impl, program);
SmokeTester smoke_tester = null;
@@ -1741,6 +1748,12 @@ namespace VC { callback.OnProgress("done", 0, 0, 1.0);
+ if (_print_time)
+ {
+ watch.Stop();
+ Console.WriteLine("Total time for this method: {0}", watch.Elapsed.ToString());
+ }
+
return outcome;
}
|