Search results

JBMC and verification of URL encoding

Status: Open.

#8630 In diffblue/cbmc;

· Etienne13 opened on Apr 22, 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

Status: Open.

Bug

#8617 In diffblue/cbmc;

· rod-chapman opened on Apr 3, 2025

CBMC getting stuck when post-processing functions with memmove and non-deterministic sizes

Status: Open.

#8615 In diffblue/cbmc;

· AmPaschal opened on Apr 2, 2025

Dump-C appears incompatible with --dfcc

Status: Open.

#8612 In diffblue/cbmc;

· tautschnig opened on Apr 2, 2025

Buggy handling of assignments involving pointer dereference

bug

Status: Open.

#8610 In diffblue/cbmc;

· nianzelee opened on Mar 31, 2025

[Question] Running CBMC on a C file with dynamic linking and/or shared libraries

question

Status: Open.

#8606 In diffblue/cbmc;

· a-shokri opened on Mar 10, 2025

[Question] Syntax Error with <code>__CPROVER_loop_invariant</code> in CBMC 6.4.1 Docker

Status: Open.

#8604 In diffblue/cbmc;

· zhoulaifu opened on Mar 5, 2025

CBMC May Struggle with <code>sscanf</code> and <code>strcmp</code> Handling in Symbolic Execution?

Status: Open.

#8602 In diffblue/cbmc;

· zhoulaifu opened on Feb 25, 2025

[QUESTION] How to log all SAT literals

Status: Open.

#8601 In diffblue/cbmc;

· cvick32 opened on Feb 25, 2025

Performance Cliff and Excessive Memory Usage at --unwind 6

Status: Open.

#8600 In diffblue/cbmc;

· zhoulaifu opened on Feb 23, 2025

__CPROVER_is_cstring() Ignored in CBMC Verification

Status: Open.

#8599 In diffblue/cbmc;

· zhoulaifu opened on Feb 21, 2025

Extracting Concrete Input Strings from CBMC Counterexamples

Status: Open.

#8598 In diffblue/cbmc;

· zhoulaifu opened on Feb 20, 2025