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

goto-instrument -dfcc spurious warnings

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

Status: Open.

#8638 In diffblue/cbmc;

· rod-chapman opened on May 11, 2025

Printing SMT file with Z3 backend crashes CBMC

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

bug

Solvers

Status: Open.

Bug

#8637 In diffblue/cbmc;

· rod-chapman opened on May 11, 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

Unbounded loop proof causes non-termination and giant SMT file

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

aws-high

bug

SMT Backend Interface

Status: Open.

#8505 In diffblue/cbmc;

· rod-chapman opened on Nov 14, 2024

Performance of framing

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

Status: Open.

#8503 In diffblue/cbmc;

· hanno-becker opened on Nov 11, 2024

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

CBMC crash if CPROVER_loop_entry is used inside an assertion inside a loop

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

bug

Status: Open.

#8453 In diffblue/cbmc;

· rod-chapman opened on Sep 13, 2024

scripts/parallel-properties.py mis-reports subprocess ABORT as TIMEOUT

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

bug

Status: Open.

#8452 In diffblue/cbmc;

· rod-chapman opened on Sep 13, 2024

Spurious warnings in proof of s2n-tls function s2n_stuffer_read_hex()

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

Status: Open.

#8427 In diffblue/cbmc;

· rod-chapman opened on Aug 27, 2024

Conflicting solver selection should make CBMC fail

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

Status: Open.

#8401 In diffblue/cbmc;

· tautschnig opened on Jul 31, 2024

Simple modular reasoning example with contracts fails

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

documentation

Status: Open.

#8367 In diffblue/cbmc;

· rod-chapman opened on Jul 3, 2024