Contracts

Issues

• Add vacuity test for contradictory requires clause

  [C] Feature / Enhancement[E] User ExperienceZ-Contracts
  Feature

  model-checking/kani#2793 · Filter by author celinval opened on Sep 28, 2023 · Contracts
  3

  

• Support for encapsulated mutability in modifies clauses

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#2907 · Filter by author JustusAdam opened on Dec 1, 2023 · Contracts
  2

  

• Missing modifies clause triggers very confusing error

  [C] BugZ-Contracts
  Bug

  model-checking/kani#3106 · Filter by author celinval opened on Mar 25, 2024 · Contracts
  

• Disallow side effects in contract expressions

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3213 · Filter by author pi314mm opened on May 30, 2024 · Contracts
  3

  

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

  [C] Bug[F] CrashZ-Contracts
  Bug

  model-checking/kani#3027 · Filter by author adpaco opened on Feb 13, 2024 · Contracts
  4

  

• Warn the user if contracts are unused

  [C] Feature / Enhancement[E] User ExperienceZ-Contracts
  Feature

  model-checking/kani#2741 · Filter by author JustusAdam opened on Sep 6, 2023 · Contracts
  

• Function Contracts: Better error messages

  [C] Feature / EnhancementT-Good First IssueZ-Contracts
  Feature

  model-checking/kani#3273 · Filter by author pi314mm opened on Jun 18, 2024 · Contracts

• Function Contracts: Mutual recursion function contract wrapper for replace code stub

  [C] Feature / EnhancementZ-Contracts
  Bug

  model-checking/kani#3316 · Filter by author pi314mm opened on Jul 2, 2024 · Contracts

• Allow users to annotate functions without body with contracts

  [C] Feature / Enhancement[E] User ExperienceZ-Contracts
  Feature

  model-checking/kani#3325 · Filter by author celinval opened on Jul 4, 2024 · Contracts
  2

• Modifies property points to a temporary variable

  [C] BugZ-Contracts
  Bug

  model-checking/kani#3336 · Filter by author celinval opened on Jul 12, 2024 · Contracts

• Function Contracts: Modifies for str

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3349 · Filter by author pi314mm opened on Jul 16, 2024 · Contracts
  

• Add support for transitive modifies clause

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3372 · Filter by author celinval opened on Jul 23, 2024 · Contracts
  1

  

• Add contract support to intrinsics

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3345 · Filter by author celinval opened on Jul 15, 2024 · Contracts

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

  [C] Feature / Enhancement[E] User ExperienceZ-Contracts
  Feature

  model-checking/kani#3396 · Filter by author adpaco opened on Jul 30, 2024 · Contracts
  

• Enable thorough Rust safety verification

  [C] Feature / EnhancementZ-Contracts
  Task

  model-checking/kani#3566 · Filter by author celinval opened on Oct 3, 2024 · Contracts
  

• Separate safety contract from correctness / panic freedom

  [C] Feature / EnhancementT-RFCZ-Contracts
  Feature

  model-checking/kani#3567 · Filter by author celinval opened on Oct 3, 2024 · Contracts
  4

  

• Create a new #[proof_for_safety(fn)]

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3579 · Filter by author celinval opened on Oct 8, 2024 · Contracts
  

• Support malloc and free in loops with loop contracts

  [C] Feature / Enhancement[F] Spurious FailureZ-Contracts
  Feature

  model-checking/kani#3587 · Filter by author qinheping opened on Oct 9, 2024 · Contracts
  

• Loop contracts in closures and coroutines

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3599 · Filter by author qinheping opened on Oct 14, 2024 · Contracts
  

• High memory consumption for interior mutability function contract test

  [C] Bug[E] PerformanceZ-Contracts
  Bug

  model-checking/kani#3611 · Filter by author zhassan-aws opened on Oct 17, 2024 · Contracts
  1

  

• Support deriving kani::Invariant for enums

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3647 · Filter by author carolynzech opened on Oct 25, 2024 · Contracts

• Proposal for new Kani API similar to CPROVER_r_ok and CPROVER_w_ok

  [C] Feature / EnhancementZ-Contracts
  Feature

  model-checking/kani#3672 · Filter by author QinyuanWu opened on Nov 1, 2024 · Contracts
  5

  

• Add option --stack-trace to print the stack trace of a failure

  [C] Feature / Enhancement[E] User ExperienceZ-Contracts
  Feature

  model-checking/kani#3681 · Filter by author celinval opened on Nov 4, 2024 · Contracts
  1

• Failed to use loop contracts to prove contracts harness for proofs with nested loops

  [C] Bug[F] Spurious FailureZ-Contracts
  Bug

  model-checking/kani#3685 · Filter by author qinheping opened on Nov 5, 2024 · Contracts
  

• Compilation Error When Stubbing Functions That Return Pointers Using Function Contracts

  [C] Bug[E] Unsupported ConstructZ-Contracts
  Feature

  model-checking/kani#3732 · Filter by author xsxszab opened on Nov 23, 2024 · Contracts
  1