Use DateTime.UtcNow instead of DateTime.Now

see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx

12 files changed, 29 insertions, 29 deletions

diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index ef9814c6..d69c624a 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -874,7 +874,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
         if (CommandLineOptions.Clo.Trace) {

           Console.WriteLine();

           Console.WriteLine("Running abstract interpretation...");

-          start = DateTime.Now;

+          start = DateTime.UtcNow;

         }

 

         WidenPoints.Compute(program);

@@ -897,7 +897,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
         program.InstrumentWithInvariants();

 

         if (CommandLineOptions.Clo.Trace) {

-          DateTime end = DateTime.Now;

+          DateTime end = DateTime.UtcNow;

           TimeSpan elapsed = end - start;

           Console.WriteLine("  [{0} s]", elapsed.TotalSeconds);

           Console.Out.Flush();

diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
index d02e6f31..f5bf1e03 100644
--- a/Source/AbsInt/NativeLattice.cs
+++ b/Source/AbsInt/NativeLattice.cs
@@ -82,7 +82,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine();

         Console.WriteLine("Running abstract interpretation...");

-        start = DateTime.Now;

+        start = DateTime.UtcNow;

       }

 

       WidenPoints.Compute(program);

@@ -103,7 +103,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       }

 

       if (CommandLineOptions.Clo.Trace) {

-        DateTime end = DateTime.Now;

+        DateTime end = DateTime.UtcNow;

         TimeSpan elapsed = end - start;

         Console.WriteLine("  [{0} s]", elapsed.TotalSeconds);

         Console.Out.Flush();

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 32c3b194..d5a98913 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -536,7 +536,7 @@ namespace Microsoft.Boogie {
 

           DateTime start = new DateTime();  // to please compiler's definite assignment rules

           if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

-            start = DateTime.Now;

+            start = DateTime.UtcNow;

             if (CommandLineOptions.Clo.Trace) {

               Console.WriteLine();

               Console.WriteLine("Verifying {0} ...", impl.Name);

@@ -584,7 +584,7 @@ namespace Microsoft.Boogie {
 

           string timeIndication = "";

 

-          DateTime end = DateTime.Now;

+          DateTime end = DateTime.UtcNow;

           TimeSpan elapsed = end - start;

           if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

             if (CommandLineOptions.Clo.Trace) {

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 6424171b..f45e2995 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -518,12 +518,12 @@ namespace Microsoft.Boogie {
       return e.ToString();

     }

 

-    private static readonly DateTime StartUp = DateTime.Now;

+    private static readonly DateTime StartUp = DateTime.UtcNow;

 

     public static void ExtraTraceInformation(string point) {

       Contract.Requires(point != null);

       if (CommandLineOptions.Clo.TraceTimes) {

-        DateTime now = DateTime.Now;

+        DateTime now = DateTime.UtcNow;

         TimeSpan timeSinceStartUp = now - StartUp;

         Console.WriteLine(">>> {0}   [{1} s]", point, timeSinceStartUp.TotalSeconds);

       }

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 1cb27648..08d8346a 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -52,11 +52,11 @@ namespace Microsoft.Boogie.Houdini {
       collector.examples.Clear();

       VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);

 

-      DateTime now = DateTime.Now;

+      DateTime now = DateTime.UtcNow;

       checker.BeginCheck(descriptiveName, vc, handler);

       WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });

       ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

-      proverTime += (DateTime.Now - now).TotalSeconds;

+      proverTime += (DateTime.UtcNow - now).TotalSeconds;

       numProverQueries++;

 

       if (proverOutcome == ProverInterface.Outcome.Invalid) {

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 2ed147d1..1f3909e4 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -103,14 +103,14 @@ namespace Microsoft.Boogie.Houdini {
       times = new IterationTimer<string>();

     }

     public override void UpdateIteration() {

-      startT = DateTime.Now;

+      startT = DateTime.UtcNow;

     }

     public override void UpdateImplementation(Implementation implementation) {

       curImp = implementation;

     }

     public override void UpdateOutcome(ProverInterface.Outcome o) {

       Contract.Assert(curImp != null);

-      DateTime endT = DateTime.Now;

+      DateTime endT = DateTime.UtcNow;

       times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique

     }

     public void PrintTimes() {

@@ -1031,7 +1031,7 @@ namespace Microsoft.Boogie.Houdini {
     private void DebugRefutedCandidates(Implementation curFunc, List<Counterexample> errors) {

       XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;

       if (xmlRefuted != null && errors != null) {

-        DateTime start = DateTime.Now;

+        DateTime start = DateTime.UtcNow;

         xmlRefuted.WriteStartMethod(curFunc.ToString(), start);

 

         foreach (Counterexample error in errors) {

@@ -1043,7 +1043,7 @@ namespace Microsoft.Boogie.Houdini {
           if (ae != null) PrintRefutedAssert(ae, xmlRefuted);

         }

 

-        DateTime end = DateTime.Now;

+        DateTime end = DateTime.UtcNow;

         xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));

       }

     }

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e837b16f..40492ce4 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -583,7 +583,7 @@ namespace Microsoft.Boogie.SMTLib
       Contract.Requires(expr != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      DateTime start = DateTime.Now;

+      DateTime start = DateTime.UtcNow;

       //if (CommandLineOptions.Clo.Trace)

       //  Console.Write("Linearising ... ");

 

@@ -621,7 +621,7 @@ namespace Microsoft.Boogie.SMTLib
       Contract.Assert(res != null);

 

       if (CommandLineOptions.Clo.Trace) {

-        DateTime end = DateTime.Now;

+        DateTime end = DateTime.UtcNow;

         TimeSpan elapsed = end - start;

         if (elapsed.TotalSeconds > 0.5)

           Console.WriteLine("Linearising   [{0} s]", elapsed.TotalSeconds);

diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index 662d45d3..b714ed67 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -201,7 +201,7 @@ USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool
       Contract.Requires(expr != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      DateTime start = DateTime.Now;

+      DateTime start = DateTime.UtcNow;

       if (CommandLineOptions.Clo.Trace)

         Console.Write("Linearising ... ");

 

@@ -238,7 +238,7 @@ USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool
       Contract.Assert(res != null);

 

       if (CommandLineOptions.Clo.Trace) {

-        DateTime end = DateTime.Now;

+        DateTime end = DateTime.UtcNow;

         TimeSpan elapsed = end - start;

         Console.WriteLine("finished   [{0} s]", elapsed.TotalSeconds);

       }

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 45f2d098..3718372b 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -296,7 +296,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       //Contract.Requires(expr != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      DateTime start = DateTime.Now;

+      DateTime start = DateTime.UtcNow;

       if (CommandLineOptions.Clo.Trace)

         Console.Write("Linearising ... ");

 

@@ -349,7 +349,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       Contract.Assert(res!=null);

 

       if (CommandLineOptions.Clo.Trace) {

-        TimeSpan elapsed = DateTime.Now - start;

+        TimeSpan elapsed = DateTime.UtcNow - start;

         Console.WriteLine("finished   [{0} s]", elapsed.TotalSeconds);

       }

       return res;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 2f7267b1..9b7b6e36 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -255,7 +255,7 @@ namespace Microsoft.Boogie {
 

       Contract.Assert(busy);

       hasOutput = true;

-      proverRunTime = DateTime.Now - proverStart;

+      proverRunTime = DateTime.UtcNow - proverStart;

 

       ProverDone.Set();

     }

@@ -272,7 +272,7 @@ namespace Microsoft.Boogie {
       outputExn = null;

       this.handler = handler;

 

-      proverStart = DateTime.Now;

+      proverStart = DateTime.UtcNow;

       thmProver.BeginCheck(descriptiveName, vc, handler);

       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 27237a51..b4e330ea 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -350,7 +350,7 @@ namespace VC
 

             public void compute(HashSet<int> goodCandidates, int bound)

             {

-                var start = DateTime.Now;

+                var start = DateTime.UtcNow;

                 goodCandidates = calls.currCandidates;

 

                 var found = 0;

@@ -427,7 +427,7 @@ namespace VC
                 }

                 checker2.Pop();

 

-                var end = DateTime.Now;

+                var end = DateTime.UtcNow;

                 Console.WriteLine("Summary computation took {0} sec and inferred {1} of {2} contracts", 

                     (end - start).TotalSeconds, found, calls.allSummaryConst.Count);

 

@@ -1334,7 +1334,7 @@ namespace VC
             Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

             // Record current time

-            var startTime = DateTime.Now;

+            var startTime = DateTime.UtcNow;

 

             // No Max: avoids theorem prover restarts

             CommandLineOptions.Clo.MaxProverMemory = 0;

@@ -1602,7 +1602,7 @@ namespace VC
             }

 

             // Record current time

-            var startTime = DateTime.Now;

+            var startTime = DateTime.UtcNow;

 

             // Run live variable analysis

             if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)

@@ -1731,7 +1731,7 @@ namespace VC
                 // Check timeout

                 if (CommandLineOptions.Clo.ProverKillTime != -1)

                 {

-                    if ((DateTime.Now - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)

+                    if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)

                     {

                         ret = Outcome.TimedOut;

                         break;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index f27da20e..6026b862 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -580,7 +580,7 @@ namespace VC {
             return false;

         }

 

-        DateTime start = DateTime.Now;

+        DateTime start = DateTime.UtcNow;

         if (CommandLineOptions.Clo.Trace) {

           System.Console.Write("    soundness smoke test #{0} ... ", id);

         }

@@ -620,7 +620,7 @@ namespace VC {
         ProverInterface.Outcome outcome = ch.ReadOutcome();

         parent.CurrentLocalVariables = null;

 

-        DateTime end = DateTime.Now;

+        DateTime end = DateTime.UtcNow;

         TimeSpan elapsed = end - start;

         if (CommandLineOptions.Clo.Trace) {

           System.Console.WriteLine("  [{0} s] {1}", elapsed.TotalSeconds,