-
Notifications
You must be signed in to change notification settings - Fork 161
OpenJul 23, 2026
No due date
•Last updated 55% complete
List view
0 of 51 selected 0 issues of 51 selected
Comprehensive Documentation of Contract Usage
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.#2747 In model-checking/kani;Add vacuity test for contradictory requires clause
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Users Should Have the Option to Opt-out of Inductive Function Contract Verification
[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.#2823 In model-checking/kani;Support for encapsulated mutability in
modifiesclauses[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.#2907 In model-checking/kani;Missing modifies clause triggers very confusing error
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Disallow side effects in contract expressions
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Contracts: Can't include non-
Copytypes in contract[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] CrashKani crashedKani crashedZ-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Warn the user if contracts are unused
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.#2741 In model-checking/kani;Ensure that reachability includes
freewhen usingassignscontracts[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.#2700 In model-checking/kani;Add support for non-deterministic pointer
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Function Contracts: Better error messages
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Function Contracts: Mutual recursion function contract wrapper for replace code stub
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Allow users to annotate functions without body with contracts
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Modifies property points to a temporary variable
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Function Contracts: Modifies for str
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Contract requirement not respected
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Add support for transitive modifies clause
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Add contract support to intrinsics
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.The
#[safety_constraint(...)]can be specified without derivingArbitraryorInvariant[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Stacked Borrows In Kani -- Extend Feature to handle more code
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.#3475 In model-checking/kani;Enable thorough Rust safety verification
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Separate safety contract from correctness / panic freedom
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Create a new
#[proof_for_safety(fn)][C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Support
mallocandfreein loops with loop contracts[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Loop contracts in closures and coroutines
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.