All issues

Search results

CBMC missing an error after exiting do-while loop

Status: Open.

#9169 In diffblue/cbmc;

· mksvoboda97 opened on Sep 24, 2026

Integer.getInteger model recurses unconditionally

Status: Open.

#9168 In diffblue/cbmc;

· lemmy opened on Sep 24, 2026

jbmc --trace prints millions of unknown characters for nondeterministic strings

Status: Open.

#9165 In diffblue/cbmc;

· lemmy opened on Sep 18, 2026

Invariant violation in fatal_assertions.cpp on a program with a failing pointer check and an mmap call

Status: Open.

#9158 In diffblue/cbmc;

· BowenWang opened on Sep 4, 2026

Documentation shows loop contracts on do/while loops, but they are rejected: the documented syntax does not parse, and do/while is unsupported by goto-instrument

Status: Open.

#9155 In diffblue/cbmc;

· rcalvom opened on Aug 11, 2026

goto-instrument --apply-loop-contracts aborts on instrument_spec_assigns.h:286 invariant when the loop write set is inferred (regression 6.3.1 → 6.6.0)

Status: Open.

#9154 In diffblue/cbmc;

· rcalvom opened on Aug 11, 2026

crash in goto-harness (nested struct with padding)

Status: Open.

#9153 In diffblue/cbmc;

· florianschanda opened on Aug 5, 2026

please add support for some missing string functions

Status: Open.

#9151 In diffblue/cbmc;

· florianschanda opened on Aug 4, 2026

SMT2 back-end emits ill-typed terms for flattened aggregates

Status: Open.

#9146 In diffblue/cbmc;

· fcasal opened on Aug 1, 2026

SMT2 back-end swaps fields in flattened overflow results

Status: Open.

#9144 In diffblue/cbmc;

· fcasal opened on Aug 1, 2026

goto-harness C output emits a spurious const on the typedef for const-qualified pointer parameters, producing non-compilable harness code

Status: Open.

#9124 In diffblue/cbmc;

· Kacha345 opened on Jul 21, 2026

static initializer of a flexible array member is silently dropped

Status: Open.

#9113 In diffblue/cbmc;

· 71iq opened on Jul 8, 2026