List view

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 contracts

Status: Open.

Feature

#2747 In model-checking/kani;

· JustusAdam opened on Sep 7, 2023

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 contracts

Status: Open.

Feature

#2793 In model-checking/kani;

· celinval opened on Sep 28, 2023

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 contracts

Status: Open.

Feature

#2823 In model-checking/kani;

· JustusAdam opened on Oct 17, 2023

Support for encapsulated mutability in modifies clauses

[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 contracts

Status: Open.

Feature

#2907 In model-checking/kani;

· JustusAdam opened on Dec 1, 2023

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 contracts

Status: Open.

Bug

#3106 In model-checking/kani;

· celinval opened on Mar 25, 2024

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 contracts

Status: Open.

Feature

#3213 In model-checking/kani;

· pi314mm opened on May 30, 2024

Contracts: Can't include non-Copy types in contract

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[F] CrashKani crashedKani crashed

Z-ContractsIssue related to code contractsIssue related to code contracts

Status: Open.

Bug

#3027 In model-checking/kani;

· adpaco-aws opened on Feb 13, 2024

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 contracts

Status: Open.

Feature

#2741 In model-checking/kani;

· JustusAdam opened on Sep 6, 2023

Ensure that reachability includes free when using assigns contracts

[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 contracts

Status: Open.

Bug

#2700 In model-checking/kani;

· JustusAdam opened on Aug 21, 2023

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 contracts

Status: Open.

Feature

#2300 In model-checking/kani;

· zpzigi754 opened on Mar 17, 2023

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 contracts

Status: Open.

Feature

#3273 In model-checking/kani;

· pi314mm opened on Jun 18, 2024

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 contracts

Status: Open.

Feature

#3316 In model-checking/kani;

· pi314mm opened on Jul 2, 2024

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 contracts

Status: Open.

Feature

#3325 In model-checking/kani;

· celinval opened on Jul 4, 2024

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 contracts

Status: Open.

Bug

#3336 In model-checking/kani;

· celinval opened on Jul 12, 2024

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 contracts

Status: Open.

Feature

#3349 In model-checking/kani;

· pi314mm opened on Jul 16, 2024

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 contracts

Status: Open.

Bug

#3370 In model-checking/kani;

· celinval opened on Jul 22, 2024

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 contracts

Status: Open.

Feature

#3372 In model-checking/kani;

· celinval opened on Jul 23, 2024

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 contracts

Status: Open.

Feature

#3345 In model-checking/kani;

· celinval opened on Jul 15, 2024

The #[safety_constraint(...)] can be specified without deriving Arbitrary or Invariant

[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 contracts

Status: Open.

Feature

#3396 In model-checking/kani;

· adpaco-aws opened on Jul 30, 2024

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 contracts

Status: Open.

Feature

#3475 In model-checking/kani;

· jsalzbergedu opened on Aug 30, 2024

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 contracts

Status: Open.

Feature

#3566 In model-checking/kani;

· celinval opened on Oct 3, 2024

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 contracts

Status: Open.

Feature

#3567 In model-checking/kani;

· celinval opened on Oct 3, 2024

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 contracts

Status: Open.

Feature

#3579 In model-checking/kani;

· celinval opened on Oct 8, 2024

Support malloc and free in 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 contracts

Status: Open.

Feature

#3587 In model-checking/kani;

· qinheping opened on Oct 9, 2024

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 contracts

Status: Open.

Feature

#3599 In model-checking/kani;

· qinheping opened on Oct 14, 2024