StandardLibrary/runtimes/net/Extern/Time.cs (43 lines of code) (raw):

// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 using System; using System.Numerics; using System.Diagnostics; using Microsoft.VisualBasic; using Wrappers_Compile; using ibyteseq = Dafny.ISequence<byte>; using byteseq = Dafny.Sequence<byte>; using icharseq = Dafny.ISequence<char>; using charseq = Dafny.Sequence<char>; namespace Time { public partial class __default { public static long CurrentRelativeTime() { var timespan = DateTime.Now - DateTime.MinValue; return (long)timespan.TotalSeconds; } public static long CurrentRelativeTimeMilli() { var timespan = DateTime.Now - DateTime.MinValue; return (long)timespan.TotalMilliseconds; } public static long GetProcessCpuTimeMillis() { return (long)Process.GetCurrentProcess().TotalProcessorTime.TotalMilliseconds; } public static _IResult<icharseq, icharseq> GetCurrentTimeStamp() { var utcTime = DateTime.UtcNow; try { // DateTime has format specifiers that make it easy to specify time stamp in different formats // using "o" as the format specifier gives us a time stamp in ISO8601 // https://learn.microsoft.com/en-us/dotnet/standard/base-types/standard-date-and-time-format-strings#Roundtrip var timestamp = utcTime.ToString("yyyy'-'MM'-'dd'T'HH':'mm':'ss'.'ffffffK"); return Result<icharseq, icharseq>.create_Success(charseq.FromString(timestamp)); } catch (Exception e) when (e is ArgumentOutOfRangeException or FormatException) { return Result<icharseq, icharseq>.create_Failure( charseq.FromString("Unable to generate timestamp in ISO8601 UTC format.")); } } } }