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

[sipma]

Unable to reproduce. The analysis reports four open 'initialized' proof obligations without crashing:

Proof Obligation Statistics for file initialized_field_memref_lookup
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Primary Proof Obligations
                                  stmt     local       api  contract      open  violated     total
--------------------------------------------------------------------------------------------------
cast                                 6         0         0         0         0         0         6
in-scope                             0         3         0         0         1         0         4
initialized                          3         4         0         0         4         0        11
lower-bound                          0         3         0         0         1         0         4
not-null                             0         0         0         0         4         0         4
stack-address-escape                 3         0         0         0         0         0         3
upper-bound                          0         3         0         0         1         0         4
valid-mem                            0         0         0         0         4         0         4
--------------------------------------------------------------------------------------------------
total                               12        13         0         0        15         0        40