Search results

Fix statement-expression expansion for Kani-provided quantifiers

bugfix

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open (in progress).

diffblue/cbmcnumber 8649

#8649 In diffblue/cbmc;

· tautschnig opened on Jun 2, 2025

Field sensitivity: account for array size in all index expressions

bugfix

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open (in progress).

diffblue/cbmcnumber 8579

#8579 In diffblue/cbmc;

· tautschnig opened on Feb 3, 2025

How does CBMC handle padding bytes?

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open.

#8499 In diffblue/cbmc;

· celinval opened on Nov 8, 2024

CBMC crashes when shadow memory used with zero-sized types

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open.

#8284 In diffblue/cbmc;

· celinval opened on May 10, 2024

Discrepancy between API specification and behavior for __CPROVER_r_ok

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

pending merge

Status: Open.

#8199 In diffblue/cbmc;

· celinval opened on Feb 8, 2024

Cleanup fmod vs IEEE remainder

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

bugfix

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Draft (not ready).

diffblue/cbmcnumber 7885

#7885 In diffblue/cbmc;

· tautschnig opened on Sep 12, 2023

<code>__CPROVER_old</code> is ignored when called form a spec function

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

Code ContractsFunction and loop contractsFunction and loop contracts

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open.

#7775 In diffblue/cbmc;

· JustusAdam opened on Jun 21, 2023

[Request] Allow function calls in quantifier bodies.

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open.

#7774 In diffblue/cbmc;

· JustusAdam opened on Jun 20, 2023

Remove <code>__CPROVER_allocated_memory</code> from <code>mman</code> modelling

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open.

#7773 In diffblue/cbmc;

· feliperodri opened on Jun 20, 2023

Add missing analysis options in verification call in C++/Rust API

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Rust APIIssues pertaining to the CBCM Rust APIIssues pertaining to the CBCM Rust API

Status: Open.

#7662 In diffblue/cbmc;

· NlightNFotis opened on Apr 11, 2023

Add missing call for C++/Rust API: <code>--ensure-one-backedge</code>

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Rust APIIssues pertaining to the CBCM Rust APIIssues pertaining to the CBCM Rust API

Status: Open.

#7661 In diffblue/cbmc;

· NlightNFotis opened on Apr 11, 2023

Add support for <code>--generate-function-body-options</code> in Rust and C++ API

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Rust APIIssues pertaining to the CBCM Rust APIIssues pertaining to the CBCM Rust API

Status: Open.

#7660 In diffblue/cbmc;

· NlightNFotis opened on Apr 11, 2023