Repository navigation

Add runtime implementation of requires and ensures #17

Closed

Labels

opened

on Jun 12, 2024

At runtime, the safety::requires and safety::ensures attributes could be converted into assert_unsafe_preconditions.

jaisnan
added
MaintenanceMaintenance related issues for the challange
on Jun 18, 2024
tautschnig commented on Mar 21, 2025
tautschnig
on Mar 21, 2025
Member
Closing as this is already implemented in Rust's contracts implementation, which we will want to use eventually.
tautschnig
closed this as completed on Mar 21, 2025
hxuhack
added a commit that references this issue on Sep 23, 2025
Merge pull request model-checking#17 from os-checker/strip-prefix-path
3932f2a
Samuelsills
added a commit that references this issue on Mar 26, 2026
Challenge 17: Verify safety of Slice functions
177a4bb
MavenRain
added a commit that references this issue on Jun 22, 2026
Format challenge model-checking#17 harnesses to satisfy upstream rustfmt
312bcc7

to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Assignees

No one assigned

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests