diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy index 057ab8d96..9125c8d31 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy @@ -23,7 +23,7 @@ module } method ESDK(config: AwsEncryptionSdkConfig) - returns (res: Result) + returns (res: Result) { var maybeCrypto := Primitives.AtomicPrimitives(); var crypto :- maybeCrypto diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy index 1d29adba5..7f8ec2943 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy @@ -52,11 +52,13 @@ module TestCreateEsdkClient { method {:test} TestClientCreation() { var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); - - expect esdk.config.commitmentPolicy == defaultConfig.commitmentPolicy.value; - expect esdk.config.maxEncryptedDataKeys == defaultConfig.maxEncryptedDataKeys; - expect esdk.config.netV4_0_0_RetryPolicy == Types.NetV4_0_0_RetryPolicy.ALLOW_RETRY; + var esdk: Types.IAwsEncryptionSdkClient :- expect EncryptionSdk.ESDK(config := defaultConfig); + expect esdk is EncryptionSdk.ESDKClient; + var esdkClient := esdk as EncryptionSdk.ESDKClient; + + expect esdkClient.config.commitmentPolicy == defaultConfig.commitmentPolicy.value; + expect esdkClient.config.maxEncryptedDataKeys == defaultConfig.maxEncryptedDataKeys; + expect esdkClient.config.netV4_0_0_RetryPolicy == Types.NetV4_0_0_RetryPolicy.ALLOW_RETRY; } method {:test} TestNetRetryFlag() {