Repository navigation
Kani reports VERIFICATION SUCCESSFUL when CBMC runs out of memory while writing its JSON results #4905
Description
If CBMC hits a std::bad_alloc while writing its --json-ui results, it still closes the partial JSON cleanly and exits with status 6. Kani ignores that exit status whenever a result array is present. It computes the verdict from a truncated list of properties. Any failures after the truncation point are dropped, so Kani can report VERIFICATION:- SUCCESSFUL and exit 0 for a harness that has a real memory-safety violation.
I tried this code:
#[kani::proof]
fn check() {
let p: *const u8;
{
let y: u8 = kani::any();
p = &y as *const u8;
}
kani::cover!(true, "reachable");
// Read through a pointer to a dead local: a memory-safety violation.
let x = unsafe { *p };
assert!(x == x);
}using the following command line invocation:
kani oom.rs
with CBMC made to fail one allocation while it writes its report. This harness is too small to run out of memory for real, so I simulated the failure on macOS with an interposed malloc that returns NULL exactly once, on the FAIL_AT-th call:
// failmalloc.c -- clang -dynamiclib -o failmalloc.dylib failmalloc.c
#include <stdlib.h>
#define DYLD_INTERPOSE(_r, _o) __attribute__((used)) static struct { const void *r; const void *o; } \
_interpose_##_o __attribute__((section("__DATA,__interpose"))) = { (const void *)&_r, (const void *)&_o };
static unsigned long count = 0, fail_at = 0; static int init = 0;
void *my_malloc(size_t sz) {
if (!init) { init = 1; const char *e = getenv("FAIL_AT"); fail_at = e ? strtoul(e, 0, 10) : 0; }
if (++count == fail_at) return NULL;
return malloc(sz);
}
DYLD_INTERPOSE(my_malloc, malloc)# wrap/cbmc -- put first on PATH
DYLD_INSERT_LIBRARIES=/path/to/failmalloc.dylib exec /opt/homebrew/bin/cbmc "$@"FAIL_AT=53600 PATH=$PWD/wrap:$PATH kani oom.rs
(The exact FAIL_AT value depends on the machine and CBMC build. Any value that lands inside CBMC's report output shows the problem.)
with Kani version: main @ c35cb96 (0.68.0), CBMC 6.10.0
I expected to see this happen: verification fails, either with the dead-object dereference failure or with Kani's "CBMC appears to have run out of memory" error.
Instead, this happened: CBMC logs Out of memory and exits with status 6. Kani reports success from the 3 properties it did receive, out of the 12 CBMC checks, and exits 0:
Out of memory
RESULTS:
Check 1: check.cover.1
- Status: SATISFIED
- Description: "reachable"
- Location: oom.rs:8:5 in function check
SUMMARY:
** 0 of 0 failed
** 1 of 1 cover properties satisfied
VERIFICATION:- SUCCESSFUL
Manual Harness Summary:
Complete - 1 successfully verified harnesses, 0 failures, 1 total.
Without the injected failure, the same harness fails as expected with check.pointer_dereference.4 ("dereference failure: dead object in *p").
Activity
Talha-Dmr commentedon Sep 29, 2026
Here is a reproducer that triggers this without fault injection. CBMC runs out of memory for real while writing the JSON trace of a property that involves a large symbolic-size allocation.
Kani 0.67.0 built from source at 152c6a8, CBMC 6.10.0, Arch Linux x86_64. It takes about 1 s and peaks at about 160 MiB RSS, so no memory limit is needed to trigger it.
Kani output (abridged):
Plain CBMC on the same goto binary (
kani --keep-temps, then Kani's own CBMC flags without--json-ui) reports the failure:(exit code 10). With
--json-uiadded, CBMC exits with status 6. Itsresultarray stops after 38 of the 253 properties, followed by{"messageText": "Out of memory", "messageType": "ERROR"}. The last property in the array iscopy_preserves_byte_mutant.reachability_check.1(status FAILURE, meaning reachable). Its trace ends partway through a step inside CBMC'smemcpymodel (<builtin-library-memcpy>).copy_preserves_byte_mutant.assertion.1never appears in the array, so Kani reports success from the 38 properties it received.We hit this on real harnesses, not only this toy. Verifying
alloc::string::String::split_offover strings of arbitrary length, a deliberately false mutant assertion got0 of 55 failed/VERIFICATION:- SUCCESSFULfrom Kani, while plain CBMC on the same goto binary reported the failure. Any harness that copies a large symbolic-size buffer (Vec/Stringof unbounded length) can hit this. Kani's reachability checks and cover properties also emit traces, so the truncation can happen even when every assertion holds.The workaround we use is to treat Kani's verdict as advisory for such harnesses. We run plain CBMC (no
--json-ui) on the--keep-tempsgoto binary and ignorereachability_check/coverFAILUREs.A fix that checks CBMC's exit status (at least status 6) when a
resultarray is present, as the issue proposes, would turn this into a clear failure.Fail verification when CBMC exits abnormally after reporting results (m…