smithy-lang / smithy-dafny

Apache License 2.0
10 stars 8 forks source link

Figure out why Error test model did not catch regression fixed by #470 #471

Open robin-aws opened 5 months ago

robin-aws commented 5 months ago

See https://github.com/smithy-lang/smithy-dafny/pull/470#issuecomment-2207492791

texastony commented 5 months ago

To be fair, I am not certain it was a regression... I think the dtor_message was always there, and never evalulated.

texastony commented 5 months ago

NVM: It was a regression. dtor_message was NOT there. https://github.com/aws/aws-cryptographic-material-providers-library/pull/466/files#diff-dd5fcb32e2c3c0081e3a9168f7ff4d1c17fcb2122f6565925dfcc103d47bd7ee