Skip to content

Commit 2bdf4f0

Browse files
committed
chore(dotnet): polymorph
1 parent 0d9b2fa commit 2bdf4f0

File tree

3 files changed

+206
-23
lines changed

3 files changed

+206
-23
lines changed

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -176,16 +176,7 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.types"
176176
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
177177
// The Opaque error, used for native, extern, wrapped or unknown errors
178178
| Opaque(obj: object)
179-
// A better Opaque, with a visible string representation.
180-
| OpaqueWithText(obj: object, objMessage : string)
181-
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
182-
// This dummy subset type is included to make sure Dafny
183-
// always generates a _ExternBase___default.java class.
184-
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
185-
predicate method IsDummySubsetType(x: int) {
186-
0 < x
187-
}
188-
179+
type OpaqueError = e: Error | e.Opaque? witness *
189180
}
190181
abstract module AbstractAwsCryptographyEncryptionSdkService
191182
{

AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -442,8 +442,6 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph
442442
new string(dafnyVal.dtor_message.Elements));
443443
case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_Opaque dafnyVal:
444444
return new OpaqueError(dafnyVal._obj);
445-
case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_OpaqueWithText dafnyVal:
446-
return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString());
447445
default:
448446
// The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?)
449447
return new OpaqueError();

0 commit comments

Comments
 (0)