Analyze COMMAREA reads through native calls

Prove a concrete short incoming length at a native CALL whose pinned callee reads the passed area on its proven entry path. Require one literal CALL and one BY REFERENCE argument. Limit the routine to one through eight letters, digits, hyphens or underscores with a leading letter or digit. Bind the complete caller and callee DISPLAY layouts by byte position and field type. Require exact source and COPY snapshots and explicit approval of normal-entry runtime binding and the same DISPLAY encoding. The callee must reach a supported character DISPLAY, MOVE or STRING read of its sole linkage parameter or a field or fixed slice within it. Permit at most 16 preceding default INITIALIZE, CONTINUE or simple EXIT statements. Initialization must affect only disjoint ordinary local storage and total at most 64 elementary writes. Branches, calls, incoming-area writes and other effects prevent this proof. MOVE reads are limited to the transferred prefix. STRING must have one incoming operand delimited by size and fit completely in a separate local character receiver. The caller uses the bounded COMMAREA entry-flow analysis. Calls remain barriers after their arrivals are observed. Unsupported interfaces, source, storage and effects cannot create a witness. Missing rows and missing findings do not establish safety. Report both source locations and conditional CWE-125 evidence. Do not change source or propose a guard. This does not establish deployed execution, allocation size, successful output, authorization or normal return.