search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 261 forks source link

Error transpiling Rust test #5924

Open ajewellamz opened 5 days ago

ajewellamz commented 5 days ago

Dafny version

4.9.1 (b998ed949)

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