Search results

Can't verify contracts for a method defined inside more than one impl block

[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: Closed (completed).

#3773 In model-checking/kani;

· by carolynzech was closed on Jan 14, 2025

· 

Function Contracts

Can't write contracts for functions that return mutable references to input arguments

[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: Closed (completed).

#3764 In model-checking/kani;

· by carolynzech was closed on Jul 4, 2025

· 

Function Contracts

Create macro to generate harnesses for contract

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Closed (completed).

#3590 In model-checking/kani;

· by celinval was closed on Jul 4, 2025

· 

Function Contracts

The order of requires clauses is 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: Not planned (skipped).

#3575 In model-checking/kani;

· by zhassan-aws was closed on Oct 15, 2024

· 

Function Contracts

ICE Resolving <code>proof_for_contract</code> target

[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: Closed (completed).

#3467 In model-checking/kani;

· by carolynzech was closed on Oct 27, 2024

· 

Function Contracts

Enable concrete playback for contract and stubs

Z-EndToEndBenchCITag a PR to run benchmark CITag a PR to run benchmark CI

Status: Merged (completed).

model-checking/kaninumber 3389

#3389 In model-checking/kani;

· by celinval was closed on Jul 31, 2024

· 

Function Contracts

Add regular &amp; fixme tests for function contracts

Z-ContractsIssue related to code contractsIssue related to code contracts

Status: Merged (completed).

model-checking/kaninumber 3371

#3371 In model-checking/kani;

· by celinval was closed on Oct 24, 2024

· 

Function Contracts

Enable contracts in associated functions

Z-ContractsIssue related to code contractsIssue related to code contracts

Z-EndToEndBenchCITag a PR to run benchmark CITag a PR to run benchmark CI

Status: Merged (completed).

model-checking/kaninumber 3363

#3363 In model-checking/kani;

· by celinval was closed on Aug 1, 2024

· 

Function Contracts

The <code>old</code> construct does not respect the function requirements

[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: Closed (completed).

#3359 In model-checking/kani;

· by celinval was closed on Sep 4, 2024

· 

Function Contracts

Function Contracts: Interior Mutability Tests

Status: Merged (completed).

model-checking/kaninumber 3351

#3351 In model-checking/kani;

· by pi314mm was closed on Jul 30, 2024

· 

Function Contracts

Add an option to turn contract clauses into assertions

[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: Closed (completed).

#3326 In model-checking/kani;

· by celinval was closed on Jan 9, 2025

· 

Function Contracts

Function Contracts: Closure Type Inference

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Z-EndToEndBenchCITag a PR to run benchmark CITag a PR to run benchmark CI

Status: Merged (completed).

model-checking/kaninumber 3307

#3307 In model-checking/kani;

· by pi314mm was closed on Jul 1, 2024

· 

Function Contracts