Initialized field proof obligation can crash on missing memory reference

[mgordon]

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.

initialized_field_memref_lookup.c