Search results

goto-instrument -dfcc spurious "no body" warnings

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

Status: Open.

#8639 In diffblue/cbmc;

· rod-chapman opened on May 15, 2025

Huge SMT file and slow proof for simple array function

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

aws-high

blocker

Code ContractsFunction and loop contractsFunction and loop contracts

pending merge

Status: Open.

Bug

#8617 In diffblue/cbmc;

· rod-chapman opened on Apr 3, 2025

Default verbosity of output when using contracts

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

Status: Open.

#8483 In diffblue/cbmc;

· rod-chapman opened on Oct 24, 2024

Function --enforce-contract causes global var precondition assertion to fail

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#8429 In diffblue/cbmc;

· BeamRaceMuppet opened on Aug 29, 2024

Better side-effect checks for loop contracts

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#8393 In diffblue/cbmc;

· qinheping opened on Jul 22, 2024

[Safety feature] Error when enforcing contracts twice

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#7830 In diffblue/cbmc;

· JustusAdam opened on Jul 27, 2023

DFCC loop contracts crashes with VS

bug

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#7807 In diffblue/cbmc;

· qinheping opened on Jul 13, 2023

Allow function call results to be interrogated with history variables

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

Status: Open.

#7802 In diffblue/cbmc;

· JustusAdam opened on Jul 7, 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

Loop assigns inference does not compute may-alias for <code>ID_member</code>.

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

Status: Open.

#7604 In diffblue/cbmc;

· qinheping opened on Mar 20, 2023

s2n_record_writev standalone example

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

do not merge

Status: Draft (not ready).

diffblue/cbmcnumber 7357

#7357 In diffblue/cbmc;

· nwetzler opened on Nov 16, 2022

Incorrect encoding of function pointer operations in CBMC

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

bug

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#7213 In diffblue/cbmc;

· feliperodri opened on Oct 5, 2022