Repository navigation
Initialized field proof obligation can crash on missing memory reference #72
Description
Initialized field proof obligation can crash on missing memory reference
Summary
During iteration 1 of a full CH-C analysis of SPEC CPU 2017 perlbench,
some initialized(...) proof obligations crashed when the checker attempted
to resolve a memory reference index that was not present in the function
environment.
Observed failures:
CCHFailure in function: Perl_pp_sort:
Failure No memory reference found with index: 57 for ppo 1588:
initialized(PL_firstgv->sv_u.svu_gp)
CCHFailure in function: Perl_pp_backtick:
Failure No memory reference found with index: 20 for ppo 234:
initialized(targ->sv_any)
Minimal repro
See initialized_field_memref_lookup.c.
The example uses global and parameter struct-pointer dereferences that force
CH-C to generate field-initialization proof obligations similar to the
PL_firstgv->sv_u.svu_gp and targ->sv_any obligations from perlbench.
Expected behavior
If the checker cannot resolve the memory reference needed to prove or refute
the initialized(...) obligation, the proof obligation should remain open with
a diagnostic explaining the missing memory reference.
Actual behavior
The checker raises CCHFailure, which terminates the per-file analysis
subprocess and prevents the project analysis from completing all files cleanly.
Minimal local workaround
Catch CCHFailure in check_initialized, add a diagnostic argument, and return
false so the obligation remains open. This is intentionally imprecise but
sound for continuing analysis of unrelated functions.
Activity
sipma commentedon Jun 18, 2026
Unable to reproduce. The analysis reports four open 'initialized' proof obligations without crashing: