Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Post 4.0, remove all code associated with :handle and :dllimport #3398

Closed
davidcok opened this issue Jan 24, 2023 · 0 comments · Fixed by #3673
Closed

Post 4.0, remove all code associated with :handle and :dllimport #3398

davidcok opened this issue Jan 24, 2023 · 0 comments · Fixed by #3673
Assignees
@davidcok
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@davidcok
Copy link
Collaborator

Summary

These attributes are deprecated with the promise of removing them entirely.
They are obsolete, undocumented, unsupported and to our knowledge, unused.

Background and Motivation

To get rid of stull that is unused, so it does not need to be maintained, tested, and documented.

Proposed Feature

Remove code

Alternatives

No response
@davidcok davidcok added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Jan 24, 2023
@davidcok davidcok self-assigned this Jan 24, 2023
@davidcok davidcok mentioned this issue Mar 2, 2023
Merged
davidcok added a commit that referenced this issue Mar 9, 2023
@davidcok
Removes deprecated attributes :dllimport :handle :heapQuantifier (#3673)
77d2953 
Fixes #3398
Follows on #3456
<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: davidcok <[email protected]>
@tchajed tchajed mentioned this issue May 10, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@davidcok davidcok

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Removes deprecated attributes :dllimport :handle :heapQuantifier davidcok/dafny
1 participant
@davidcok