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.

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

Separate safety contract from correctness / panic freedom #3567

Open
Tracked by #3566
celinval opened this issue Oct 3, 2024 · 0 comments
Open
Tracked by #3566

Separate safety contract from correctness / panic freedom #3567

celinval opened this issue Oct 3, 2024 · 0 comments

Comments

@celinval
Copy link
Contributor

celinval commented Oct 3, 2024

Users should be able to annotate their unsafe functions with safety conditions and to differentiate between safety and panic freedom / correctness properties.

For example, the Index function index and the slice get_unchecked have the same pre-conditions, however, violating these conditions have very different consequences. Many users of index rely on the fact that it will panic if their assumptions about the index is incorrect. Thus, their contracts should reflect this difference.

@celinval celinval changed the title Modify its contract annotation to allow users to specify safety contract separate from correctness / panic freedom. Safety contract should only be accepted in unsafe funtions. Separate safety contract from correctness / panic freedom Oct 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant