Null-terminated proof check crashes on cast startof stack buffer expression

[mgordon]

Null-terminated proof check crashes on cast startof stack buffer expression

Summary

During SPEC CPU 2017 perlbench analysis, CH-C crashes while checking a
null-terminated proof obligation over a cast startof expression for a local
stack buffer. The concrete failure is in mg:Perl_magic_setenv during analysis
iteration 1:

CCHFailure in function: Perl_magic_setenv:
Failure No memory reference found with index: 14 for ppo 389:
null-terminated(caste (startof (tmpbuf):(char*)))

Small reproducer

See null_terminated_cast_startof.c.

extern void consume_string(char *);

void null_terminated_cast_startof(int flag) {
  char tmpbuf[8];

  tmpbuf[0] = 'x';
  tmpbuf[1] = 0;

  if (flag) {
    consume_string((char *)&tmpbuf);
  } else {
    consume_string((char *)tmpbuf);
  }
}

The first call shape is intended to mimic the perlbench obligation shape where
the checker sees a cast around the start address of a local array.

Observed behavior

The proof obligation checker attempts to resolve a memory reference for the
expression and raises CCHFailure when the memory-reference table does not
contain the expected index. This aborts the whole file analysis rather than
leaving the single proof obligation open.

Expected behavior

The analyzer should not crash. Either:

1. Recognize casted startof local array expressions as stack-memory addresses
   and use existing null-termination reasoning, or
2. Leave the null-terminated obligation open with a diagnostic when the memory
   reference cannot be resolved.

Minimal local workaround

For the perlbench run, the null-terminated checker was wrapped in a narrow
CCHFailure catch that records a diagnostic and returns false, leaving the
proof obligation open. This is intentionally imprecise but allows complete
project analysis to proceed.

null_terminated_cast_startof.c

[sipma]

Unable to reproduce the failure with the given reproducer program. The reproducer program does not generate any null-terminated proof obligations. All 16 of the proof obligations generated are discharged at the statement level, so no further analysis is performed.

Primary Proof Obligations
                                  stmt     local       api  contract      open  violated     total
--------------------------------------------------------------------------------------------------
in-scope                             2         0         0         0         0         0         2
index-lower-bound                    2         0         0         0         0         0         2
index-upper-bound                    2         0         0         0         0         0         2
initialized                          1         0         0         0         0         0         1
lower-bound                          2         0         0         0         0         0         2
pointer-cast                         1         0         0         0         0         0         1
signed-to-signed-cast-lb             1         0         0         0         0         0         1
signed-to-signed-cast-ub             1         0         0         0         0         0         1
upper-bound                          2         0         0         0         0         0         2
valid-mem                            2         0         0         0         0         0         2
--------------------------------------------------------------------------------------------------
total                               16         0         0         0         0         0        16