Skip to content

Error transpiling Rust test #5924

Open
Open
@ajewellamz

Description

@ajewellamz

Dafny version

4.9.1 (b998ed9)

Code to produce this issue

git clone --recurse-submodules git@github.com:aws/aws-cryptographic-material-providers-library.git

Command to run and resulting output

cd TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/VectorsComposition

dafny test -t rs --function-syntax 3 AllRequiredEncryptionContextCmm.dfy

What happened?

(0,-1): Error: Microsoft.Dafny.UnsupportedInvalidOperationException: Could not generate coercion function for contructor 1 of Bracketed

As part of the regular MPL build, this file produces Rust code with no complaint.

What type of operating system are you experiencing the problem on?

Mac

Metadata

Metadata

Assignees

No one assigned

    Labels

    crashDafny crashes on this input, or generates malformed code that can not be executedkind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labellang: rustDafny's transpiler to Rust and its runtime

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions