You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
initialized-range over casted startof can abort on missing memory reference #73
initialized-range over casted startof can abort on missing memory reference
Summary
During perlbench iteration 1, CH-C aborts while checking an initialized-range
proof obligation if the base expression is a casted start-of-stack-array
expression and the corresponding memory-reference id cannot be resolved.
In SPEC CPU 2017 perlbench, the second analysis round failed in mg:Perl_magic_setenv with:
CCHFailure in function: Perl_magic_setenv:
Failure No memory reference found with index: 14 for ppo 391:
initialized-range(caste (startof (tmpbuf):(char*)),
ntp[caste (startof (tmpbuf):(char*))])
The exception is raised from memory_reference_manager_t#get_memory_reference
and propagates out of check_initialized_range, causing the whole file
analysis subprocess to fail.
Minimal Workaround
For the SPEC perlbench run, the checker now catches CCHFailure inside check_initialized_range, records the message as a diagnostic argument, and
returns false. This leaves the specific proof obligation open instead of
crashing the project analysis.
Suggested Proper Fix
The better fix is to preserve/reconstruct the memory reference for casted startof(array) expressions so that initialized-range can reason about the
underlying stack array. The current workaround intentionally sacrifices
precision only for this failing obligation.
Activity
sipma commentedon Jun 18, 2026
Unable to reproduce. The initialized-range proof obligation is reported open, without causing a crash on the reproducer program.