From 5669e0b709b29612f3177802fce57bcd9ff7ea90 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Mon, 28 Oct 2024 15:33:36 -0400 Subject: [PATCH] fix: repolymorph to get default parameter for OpaqueError (#911) * fix: repolymorph to get default parameter for OpaqueError --- .../Model/AwsCryptographyMaterialProvidersTypes.dfy | 2 +- .../Model/AwsCryptographyKeyStoreTypes.dfy | 2 +- .../Model/AwsCryptographyPrimitivesTypes.dfy | 2 +- ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy | 2 +- ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy | 2 +- .../AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy | 2 +- smithy-dafny | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy index b0372e8a9..a84587ea0 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy @@ -1712,7 +1712,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty // || (!exit(A(I)) && !access(B(I))) | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) + | Opaque(obj: object, alt_text : string := "") type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractAwsCryptographyMaterialProvidersService diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy index 0fad1ce05..bf5d9450f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy @@ -282,7 +282,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw // || (!exit(A(I)) && !access(B(I))) | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) + | Opaque(obj: object, alt_text : string := "") type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractAwsCryptographyKeyStoreService diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy index e442b0fff..a01e74bd8 100644 --- a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy +++ b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy @@ -689,7 +689,7 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" } // || (!exit(A(I)) && !access(B(I))) | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) + | Opaque(obj: object, alt_text : string := "") type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractAwsCryptographyPrimitivesService diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy index dec776c14..b42a06773 100644 --- a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy +++ b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy @@ -2725,7 +2725,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) + | Opaque(obj: object, alt_text : string := "") type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractComAmazonawsDynamodbService { diff --git a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy index 6132487cb..a8a16c66a 100644 --- a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy +++ b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy @@ -1976,7 +1976,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types" // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) + | Opaque(obj: object, alt_text : string := "") type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractComAmazonawsKmsService { diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy index 7d9894703..f37e544cf 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy @@ -260,7 +260,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in // || (!exit(A(I)) && !access(B(I))) | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) + | Opaque(obj: object, alt_text : string := "") type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService diff --git a/smithy-dafny b/smithy-dafny index e602cbf45..cff81f5ba 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit e602cbf45e55108f3a753c1ea06d38bd5fcdbe3c +Subproject commit cff81f5baa7104f6873aadc81d8e9a75121253cd