Skip to content

Commit 6118d8a

Browse files
committed
chore(dafny): add timing support
1 parent 4f18689 commit 6118d8a

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
2121
import JsonConfig
2222
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
2323
import KeyVectors
24+
import OsLang
2425

2526
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient)
2627
returns (output : Result<bool, string>)
@@ -110,6 +111,14 @@ module {:options "-functionSyntax:4"} DecryptManifest {
110111
}
111112
}
112113

114+
function LogFileName() : string
115+
{
116+
if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
117+
"..\\..\\PerfLog.txt"
118+
else
119+
"../../PerfLog.txt"
120+
}
121+
113122
method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
114123
returns (output : Result<bool, string>)
115124
requires keyVectors.ValidState()
@@ -168,11 +177,13 @@ module {:options "-functionSyntax:4"} DecryptManifest {
168177
}
169178
}
170179

180+
var time := Time.GetAbsoluteTime();
171181
for i := 0 to |tests.value| {
172182
var obj := tests.value[i];
173183
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
174184
var _ :- OneTest(obj.0, obj.1, keyVectors);
175185
}
186+
Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName()));
176187

177188
timeStamp :- expect Time.GetCurrentTimeStamp();
178189
print timeStamp + " Tests Complete.\n";

0 commit comments

Comments
 (0)