generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 11
Open
Labels
soundnessBugs that cause the generated code to compute the wrong value or crashBugs that cause the generated code to compute the wrong value or crash
Description
Follow up from #752 which disabled this in Rust.
The SDKs will produce values that violate constraints, such as a Some({}) on an optional map with @Length(min: 1). This could be considered an SDK bug since information is lost, SDKs are also not supposed to validate constraints, which makes it harder to argue it should be fixed. At the same time the types we generate for Dafny AWS SDKs assume these constraints are satisfied, so by not validating we are introducing unsoundness in the Dafny code.
The proper fix is likely a pretty big refactoring to distinguish which Dafny interfaces MUST assume constraints are satisfied (what the Smithy specification calls authoritative implementations) and which SHOULD NOT.
Metadata
Metadata
Assignees
Labels
soundnessBugs that cause the generated code to compute the wrong value or crashBugs that cause the generated code to compute the wrong value or crash