Find COBOL COMMAREA copy lengths

Track incoming byte counts through structured IF checks before direct character MOVEs from an explicitly configured COMMAREA. Report an admitted short length that reaches a copy before an unsupported statement. The proof includes text fields and alphanumeric groups in records of PIC X and unsigned DISPLAY PIC 9 integer fields. Receivers must be standalone PIC X items. Required received lengths include field offsets. Elementary numeric moves remain unsupported. Accept table-free source slices with positive literal positions and lengths that fit the declared source. An omitted length extends to the source field end. Include the slice position in the required received length and limit copied bytes to the receiver width. Dynamic or invalid slices and sliced receivers remain unsupported. Track integer and supported LENGTH OF comparisons with AND, OR, NOT and parentheses. Bound each condition to 64 terms and 16 parenthesis levels. Preserve exact admitted length sets and normal AND precedence. Unrelated fields, abbreviated comparisons and unsupported terms invalidate the whole condition. CONTINUE, simple EXIT, GOBACK and normal paragraph fallthrough are modeled. Literal assignments to supported disjoint ordinary scalar fields preserve incoming counts. Assignments to the received-length field and unknown sources stop the proof. Resolved data copybooks can supply layouts. Follow direct jumps to uniquely named paragraphs or sections, including cycles. Join exact admitted length sets without loop unrolling. Calls, computed or ambiguous jumps, other effects, incomplete source and uncertain storage stop the proof on that path. The analysis does not establish caller reachability or choose a failure exit. Missing findings do not establish safety. Simple EXIT preserves admitted lengths and continues to the next statement. Other EXIT forms remain outside this proof. Plain DISPLAY of quoted ASCII text preserves local fields and does not inspect a status value or terminate processing. Accept at most 16 literals of at most 256 characters each. Device options, screen positioning, exception clauses, field reads and functions remain barriers. Preserve incoming lengths across supported SET condition-name TO TRUE assignments to separate ordinary standalone fields. Every target must be disjoint from the received length. Validate all declarations and targets under the existing 16-target and 64-value limits. Writes to the byte count or incoming area and unsupported SET forms remain flow barriers. Setting an error flag does not reject an entry. Preserve incoming lengths across plain INITIALIZE of disjoint ordinary local fields and groups. Validate all targets and members within 16 targets and 64 elementary writes. Writes to the received count or incoming area, unknown targets, aliases and unsupported storage remain flow barriers. Replacement phrases are not modeled. Initializing an error record does not reject short input or establish received bytes. Follow numeric EVALUATE of the configured received count with at most 64 literal WHEN choices and 16 nested selections. Support integer literals of at most 18 digits, inclusive ascending THRU ranges and shared WHEN choices. Use the first matching branch. Unmatched lengths take WHEN OTHER or continue after END-EVALUATE. Validate every label before selecting any branch. Other subjects, ALSO, variable bounds and unsupported choices remain barriers. Branch effects keep their existing rules. Unknown paths do not manufacture received-length witnesses. Follow GO TO paragraph targets qualified by IN or OF when both the named section and its paragraph are unique. Use the resolved declaration, including empty paragraphs and backward jumps. Ambiguous sections, duplicate paragraphs within a section, missing targets and computed jumps remain flow barriers. Qualification does not bypass existing source, storage or statement-effect checks. Preserve incoming lengths across bounded STRING DELIMITED BY SIZE into separate ordinary PIC X storage. Require every field operand to be ordinary local storage and the complete write to fit its receiver. Limit operands to 16 and fields to 256 characters. Writes to the received count or incoming area, direct incoming-area reads, overlap, pointers, overflow handlers and unsupported forms remain barriers. Constructing an error message does not reject an entry or establish received bytes. Treat exact EXEC CICS RETURN END-EXEC without options as leaving the current CICS logical level. Remove only the incoming lengths that take that branch. Preserve earlier access witnesses and unresolved effects. This does not establish whole-task termination. Other RETURN forms remain unsupported. Accept the standard system-supplied DFHEIBLK.EIBCALEN group member under an explicit entry contract. Require ordinary source, unique translator fields and disjoint incoming storage. Accept plain resolved data COPY declarations after validating their source and expanded declaration words. Reject replacement and library phrases, nested copies, procedural copies, explicit interface copies and copied directives. Custom interface declarations, shadow fields, aliases and source-mode barriers remain unsupported. Retain concrete native counts through 9999 when a larger entry interval is admitted. Represent the rest as unknown without manufacturing witnesses. When no concrete short witness is proven and higher counts remain unmodeled, report UNRESOLVED_ENTRY_LENGTHS. That status does not claim an unknown path reaches the operation. Native halfword capacity does not establish compiler comparison semantics above 9999. Writes to the field or its enclosing interface invalidate the entry value. The contract still supplies caller admission and actual received-count meaning. INITIALIZE VALUE and FILLER phrases require a separate effect proof and discard default-assignment facts. An explicit TO DEFAULT without a VALUE, FILLER or replacement phrase retains the default behavior. Preserve known received counts after a supported incoming-area MOVE or plain character DISPLAY only when they cover its complete read extent. Keep paths with an earlier short read unknown. They cannot authorize a later guard insertion. Successful output remains unproven.