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

goto-symex: assumed pointer equalities must update value set

bugfix

Symbolic Execution

Status: Open (in progress).

diffblue/cbmcnumber 8494

#8494 In diffblue/cbmc;

· tautschnig opened on Nov 4, 2024

goto-symex: move level1 map to goto_statet

bugfix

Symbolic Execution

Status: Open (in progress).

diffblue/cbmcnumber 8439

#8439 In diffblue/cbmc;

· tautschnig opened on Sep 3, 2024

Support comparing arrays of non-constant size with array_equal

aws-high

bugfix

Symbolic Execution

Status: Open (in progress).

diffblue/cbmcnumber 8208

#8208 In diffblue/cbmc;

· tautschnig opened on Feb 16, 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

Use extractbits to extract non-byte-fields from unions

bugfix

Status: Draft (not ready).

diffblue/cbmcnumber 7861

#7861 In diffblue/cbmc;

· tautschnig opened on Aug 21, 2023

Variadic args/va_arg: handle unexpected va_list types

bugfix

Status: Open (in progress).

diffblue/cbmcnumber 7711

#7711 In diffblue/cbmc;

· tautschnig opened on May 15, 2023

C front-end: ensure array type updates are consistent

bugfix

C Front End

Status: Open (in progress).

diffblue/cbmcnumber 7610

#7610 In diffblue/cbmc;

· tautschnig opened on Mar 22, 2023

Linking: fix up all types before handling functions or objects

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

bugfix

Status: Open (in progress).

diffblue/cbmcnumber 7579

#7579 In diffblue/cbmc;

· tautschnig opened on Mar 7, 2023

Expanding __CPROVER_{r,w,rw}_ok must not introduce overflow [depends-on: #6616]

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

bugfix

dependent - do not merge

Property Instrumentation

Status: Open (in progress).

diffblue/cbmcnumber 6656

#6656 In diffblue/cbmc;

· tautschnig opened on Feb 10, 2022

goto_check_c: observe check pragmas annotated to individual expressions

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

blocker

bugfix

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

Property Instrumentation

Status: Open (in progress).

diffblue/cbmcnumber 6616

#6616 In diffblue/cbmc;

· tautschnig opened on Jan 30, 2022