diff --git a/TestModels/CallingAWSSDKFromLocalService/Model/CallingAWSSDKFromLocalService.smithy b/TestModels/CallingAWSSDKFromLocalService/Model/CallingAWSSDKFromLocalService.smithy index edc289517..457e4e60d 100644 --- a/TestModels/CallingAWSSDKFromLocalService/Model/CallingAWSSDKFromLocalService.smithy +++ b/TestModels/CallingAWSSDKFromLocalService/Model/CallingAWSSDKFromLocalService.smithy @@ -49,7 +49,6 @@ structure CallDDBScanInput { } structure CallDDBScanOutput { - @required itemOutput: com.amazonaws.dynamodb#Integer, } @@ -68,7 +67,6 @@ structure CallDDBGetItemInput { } structure CallDDBGetItemOutput { - @required itemOutput: com.amazonaws.dynamodb#AttributeMap, } @@ -107,7 +105,6 @@ structure CallKMSEncryptInput { } structure CallKMSEncryptOutput { - @required encryptOutput: com.amazonaws.kms#KeyIdType, } @@ -126,9 +123,7 @@ structure CallKMSDecryptInput { } structure CallKMSDecryptOutput { - @required KeyIdType: com.amazonaws.kms#KeyIdType, - @required Plaintext: com.amazonaws.kms#PlaintextType } diff --git a/TestModels/CallingAWSSDKFromLocalService/src/SimpleCallingawssdkfromlocalserviceImpl.dfy b/TestModels/CallingAWSSDKFromLocalService/src/SimpleCallingawssdkfromlocalserviceImpl.dfy index ad2776655..8316fccf9 100644 --- a/TestModels/CallingAWSSDKFromLocalService/src/SimpleCallingawssdkfromlocalserviceImpl.dfy +++ b/TestModels/CallingAWSSDKFromLocalService/src/SimpleCallingawssdkfromlocalserviceImpl.dfy @@ -47,7 +47,7 @@ module SimpleCallingawssdkfromlocalserviceImpl refines AbstractSimpleCallingawss ); var retScan := input.ddbClient.Scan(ScanInput); if retScan.Success? { - return Success(CallDDBScanOutput(itemOutput := retScan.value.Count.UnwrapOr(-1))); + return Success(CallDDBScanOutput(itemOutput := retScan.value.Count)); } else { return Failure(ComAmazonawsDynamodb(retScan.error)); } @@ -62,7 +62,7 @@ module SimpleCallingawssdkfromlocalserviceImpl refines AbstractSimpleCallingawss var retGetItem := input.ddbClient.GetItem(GetItemInput); var emptyMap : Dynamodb.Types.AttributeMap := map[]; if retGetItem.Success? { - return Success(CallDDBGetItemOutput(itemOutput := retGetItem.value.Item.UnwrapOr(emptyMap))); + return Success(CallDDBGetItemOutput(itemOutput := retGetItem.value.Item)); } else { return Failure(ComAmazonawsDynamodb(retGetItem.error)); } @@ -95,7 +95,7 @@ module SimpleCallingawssdkfromlocalserviceImpl refines AbstractSimpleCallingawss ); var retEncryptResponse := input.kmsClient.Encrypt(encryptInput); if retEncryptResponse.Success? { - return Success(CallKMSEncryptOutput(encryptOutput := retEncryptResponse.value.KeyId.UnwrapOr("DummyString"))); + return Success(CallKMSEncryptOutput(encryptOutput := retEncryptResponse.value.KeyId)); } else { return Failure(Types.ComAmazonawsKms(retEncryptResponse.error)); } @@ -108,9 +108,8 @@ module SimpleCallingawssdkfromlocalserviceImpl refines AbstractSimpleCallingawss KeyId := Wrappers.Some(input.keyId) ); var retDecryptResponse := input.kmsClient.Decrypt(decryptInput); - var emptyPlainText : Kms.Types.PlaintextType := [ 0 ]; if retDecryptResponse.Success? { - return Success(CallKMSDecryptOutput(KeyIdType := retDecryptResponse.value.KeyId.UnwrapOr("DummyString"), Plaintext := retDecryptResponse.value.Plaintext.UnwrapOr(emptyPlainText))); + return Success(CallKMSDecryptOutput(KeyIdType := retDecryptResponse.value.KeyId, Plaintext := retDecryptResponse.value.Plaintext)); } else { return Failure(Types.ComAmazonawsKms(retDecryptResponse.error)); } diff --git a/TestModels/CallingAWSSDKFromLocalService/test/SimpleCallingawssdkfromlocalserviceImplTest.dfy b/TestModels/CallingAWSSDKFromLocalService/test/SimpleCallingawssdkfromlocalserviceImplTest.dfy index f3b6a330a..57e0a4aa9 100644 --- a/TestModels/CallingAWSSDKFromLocalService/test/SimpleCallingawssdkfromlocalserviceImplTest.dfy +++ b/TestModels/CallingAWSSDKFromLocalService/test/SimpleCallingawssdkfromlocalserviceImplTest.dfy @@ -45,7 +45,7 @@ module SimpleCallingawssdkfromlocalserviceImplTest { var resSuccess := client.CallDDBScan(SimpleCallingawssdkfromlocalservice.Types.CallDDBScanInput(ddbClient := ddbClient, tableArn := TABLE_ARN_SUCCESS_CASE)); expect resSuccess.Success?; - expect resSuccess.value.itemOutput != -1; + expect resSuccess.value.itemOutput.Some?; } method TestCallDDBScan_Failure(client: ISimpleCallingAWSSDKFromLocalServiceClient) @@ -80,8 +80,8 @@ module SimpleCallingawssdkfromlocalserviceImplTest { var resSuccess := client.CallDDBGetItem(SimpleCallingawssdkfromlocalservice.Types.CallDDBGetItemInput(ddbClient := ddbClient, tableArn := TABLE_ARN_SUCCESS_CASE, key := Key2Get)); expect resSuccess.Success?; - // expect resSuccess.value.itemOutput; - var output := resSuccess.value.itemOutput; + expect resSuccess.value.itemOutput.Some?; + var output := resSuccess.value.itemOutput.value; expect output.Keys == {"branch-key-id", "version", "create-time", "enc", "hierarchy-version", "status"}; expect |output.Keys| == |output.Values|; @@ -161,7 +161,8 @@ module SimpleCallingawssdkfromlocalserviceImplTest { var resSuccess := client.CallKMSEncrypt(SimpleCallingawssdkfromlocalservice.Types.CallKMSEncryptInput(kmsClient := kmsClient, keyId := KEY_ID_SUCCESS_CASE, plaintext := PLAIN_TEXT)); expect resSuccess.Success?; - expect resSuccess.value.encryptOutput == KEY_ID_SUCCESS_CASE; + expect resSucess.value.encryptOutput.Some?; + expect resSuccess.value.encryptOutput.value == KEY_ID_SUCCESS_CASE; } method TestCallKMSEncrypt_Failure(client: ISimpleCallingAWSSDKFromLocalServiceClient) @@ -214,8 +215,10 @@ module SimpleCallingawssdkfromlocalserviceImplTest { var resSuccess := client.CallKMSDecrypt(SimpleCallingawssdkfromlocalservice.Types.CallKMSDecryptInput(kmsClient := kmsClient, keyId := KEY_ID_SUCCESS_CASE, ciphertextBlob := workAround(CiphertextBlob))); expect resSuccess.Success?; - expect resSuccess.value.KeyIdType == KEY_ID_SUCCESS_CASE; - expect resSuccess.value.Plaintext == [ 165, 191, 67, 62 ]; + expect resSuccess.value.KeyIdType.Some?; + expect resSuccess.value.Plaintext.Some?; + expect resSuccess.value.KeyIdType.value == KEY_ID_SUCCESS_CASE; + expect resSuccess.value.Plaintext.value == [ 165, 191, 67, 62 ]; } method TestCallKMSDecrypt_Failure(client: ISimpleCallingAWSSDKFromLocalServiceClient)