-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Shubham Chaturvedi
committed
Sep 12, 2024
1 parent
dbb8c6d
commit d24ca4d
Showing
3 changed files
with
101 additions
and
0 deletions.
There are no files selected for viewing
38 changes: 38 additions & 0 deletions
38
TestModels/aws-sdks/kms/runtimes/go/ImplementationFromDafny-go/Com_Amazonaws_Kms/extern.go
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
package Com_Amazonaws_Kms | ||
|
||
import ( | ||
"context" | ||
|
||
"github.com/aws/aws-sdk-go-v2/config" | ||
"github.com/aws/aws-sdk-go-v2/service/kms" | ||
_dafny "github.com/dafny-lang/DafnyRuntimeGo/dafny" | ||
"github.com/dafny-lang/DafnyStandardLibGo/Wrappers" | ||
ComAmazonawsKmsTypes "github.com/smithy-lang/smithy-dafny/kms/ComAmazonawsKmsTypes" | ||
"github.com/smithy-lang/smithy-dafny/kms/KMSwrapped" | ||
) | ||
|
||
func (_static *CompanionStruct_Default___) KMSClient() Wrappers.Result { | ||
cfg, err := config.LoadDefaultConfig(context.TODO(), config.WithSharedConfigProfile("default")) | ||
if err != nil { | ||
panic(err) | ||
} | ||
return Wrappers.Companion_Result_.Create_Success_(&KMSwrapped.Shim{Client: kms.NewFromConfig(cfg, func(o *kms.Options) { | ||
o.Region = "us-west-2" | ||
})}) | ||
} | ||
|
||
func (_static *CompanionStruct_Default___) RegionMatch(k ComAmazonawsKmsTypes.IKMSClient, S _dafny.Sequence) Wrappers.Option { | ||
var r = func() *string { | ||
var s string | ||
for i := _dafny.Iterate(S); ; { | ||
val, ok := i() | ||
if !ok { | ||
return &[]string{s}[0] | ||
} else { | ||
s = s + string(val.(_dafny.Char)) | ||
} | ||
} | ||
}() | ||
var nc = k.(*KMSwrapped.Shim).Client | ||
return Wrappers.Companion_Option_.Create_Some_(nc.Options().Region == *r) | ||
} |
30 changes: 30 additions & 0 deletions
30
TestModels/aws-sdks/kms/runtimes/go/ImplementationFromDafny-go/go.mod
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
module github.com/smithy-lang/smithy-dafny/kms | ||
|
||
go 1.23.0 | ||
|
||
//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381 | ||
replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../../DafnyRuntimeGo/ | ||
|
||
replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ | ||
|
||
require ( | ||
github.com/aws/aws-sdk-go-v2/config v1.27.33 | ||
github.com/aws/aws-sdk-go-v2/service/kms v1.35.5 | ||
github.com/dafny-lang/DafnyRuntimeGo v0.0.0-00010101000000-000000000000 | ||
github.com/dafny-lang/DafnyStandardLibGo v0.0.0-00010101000000-000000000000 | ||
) | ||
|
||
require ( | ||
github.com/aws/aws-sdk-go-v2 v1.30.5 // indirect | ||
github.com/aws/aws-sdk-go-v2/credentials v1.17.32 // indirect | ||
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.13 // indirect | ||
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 // indirect | ||
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 // indirect | ||
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.19 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/sso v1.22.7 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.26.7 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/sts v1.30.7 // indirect | ||
github.com/aws/smithy-go v1.20.4 // indirect | ||
) |
33 changes: 33 additions & 0 deletions
33
TestModels/aws-sdks/kms/runtimes/go/TestsFromDafny-go/go.mod
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
module github.com/smithy-lang/smithy-dafny/kms/test | ||
|
||
go 1.23.0 | ||
|
||
replace github.com/smithy-lang/smithy-dafny/kms v0.0.0 => ../ImplementationFromDafny-go | ||
|
||
//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381 | ||
replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../../DafnyRuntimeGo/ | ||
|
||
replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ | ||
|
||
require ( | ||
github.com/aws/aws-sdk-go-v2/service/kms v1.35.5 | ||
github.com/dafny-lang/DafnyRuntimeGo v0.0.0-00010101000000-000000000000 | ||
github.com/dafny-lang/DafnyStandardLibGo v0.0.0-00010101000000-000000000000 | ||
github.com/smithy-lang/smithy-dafny/kms v0.0.0 | ||
) | ||
|
||
require ( | ||
github.com/aws/aws-sdk-go-v2 v1.30.5 // indirect | ||
github.com/aws/aws-sdk-go-v2/config v1.27.33 // indirect | ||
github.com/aws/aws-sdk-go-v2/credentials v1.17.32 // indirect | ||
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.13 // indirect | ||
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 // indirect | ||
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 // indirect | ||
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.19 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/sso v1.22.7 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.26.7 // indirect | ||
github.com/aws/aws-sdk-go-v2/service/sts v1.30.7 // indirect | ||
github.com/aws/smithy-go v1.20.4 // indirect | ||
) |