Fix more issues in the Dafny-to-Rust compiler - Githubissues

dafny-lang / dafny

Dafny is a verification-aware programming language

https://dafny.org

Other

2.94k stars 261 forks source link

Fix more issues in the Dafny-to-Rust compiler #5926

Closed MikaelMayer closed 4 days ago

MikaelMayer commented 5 days ago

Description

Fixes #5923
Fixes ownership issues when an expression is the object on which to call a method or a function (auto-borrowed)
Equality on boolean newtypes now returns the newtype itself as expected
Less than now accepts newtype expressions but returns bools
Fixed bit vector truncation when the two types align and replaced the wrong bitwise negation from "~" to "!" and it's now tested.
Fixed support for testing primitive ints against test synonyms

How has this been tested?

I added originally failing tests to comp/rust/newtypes.dfy and verified that this PR fixed them

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.