Analyze COBOL COMMAREA forwarding lengths

Track incoming byte counts before LINK or XCTL forwards an explicitly configured COMMAREA. Report an admitted short length that reaches a command advertising more bytes than were received. Require one complete CICS command with a literal PROGRAM name, the unchanged top-level incoming area and an exact LENGTH from 1 through 32763 within its declared DISPLAY layout. Only PROGRAM, COMMAREA, LENGTH and optional NOHANDLE are supported. Unknown lengths, slices, additional options and multiple EXEC islands remain unresolved. Accept a written length or an exact local value in a standalone ordinary S9(4) COMP, COMPUTATIONAL or BINARY field. Record the supporting assignments. Declaration VALUE clauses do not establish an entry value. The incoming-length proof still stops at operations it does not model, even if a separate local-value analysis knows the length. Share the finite entry-flow model used for COMMAREA copies. It follows supported IF conditions, direct jumps, paragraph fallthrough, disjoint literal assignments and plain literal messages. Earlier copies remove lengths that would already overread. CICS commands, calls, changes to the area or length and other unknown effects stop propagation. The explicit contract supplies normal-entry reachability and every admitted integer length. Incomplete source and unsupported storage stop the proof. This proves a forwarded length mismatch. It does not prove command success, an actual callee read, authorization or a safe failure exit. No code is changed except optional search markers. 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. A supported SET can assign a separate binary halfword forwarding length. The local value proof must still establish one value at the command. Filter at most 16 known integer candidates after a direct IF whose rejected branch ends in GOBACK, plain CICS RETURN or a proven jump to a terminal exit. Require one ordinary integer field, fully understood comparisons and no ELSE. Permit only simple no-ops and literal messages before the exit. Limit the branch to 16 statements and evidence to 64 steps. Keep only candidates for which the condition is false. Unknown conditions and empty continuing sets discard local facts. This does not establish reachability or summarize exits in performed paragraphs. Filter known PIC X candidates after a direct IF without ELSE. Require GOBACK, plain CICS RETURN or a proven jump to a terminal exit on the rejected branch. Evaluate only equal and not-equal comparisons on one field with ASCII literals or spaces. Apply space padding to the shorter operand and preserve case. Validate every Boolean term. Reject explicit compiler options, debugging mode and copied environment declarations in the current or enclosing programs. Also reject any program collating sequence in those programs. Retain at most 16 candidates and 64 evidence steps. Permit at most 16 rejection statements consisting of simple no-ops, literal messages and the final exit. Unknown conditions and empty continuing sets discard local facts. The surviving characters can also supply a local trailing-trim length. No entry value, route approval or reachability is inferred from a guard alone. Also accept a direct GO TO rejection when a bounded local path proves that it reaches a supported terminal exit. Inspect each jump path within 64 statements and 16 paragraphs. Follow only uniquely resolved paragraphs before unconditional tail jumps or the final exit. Permit simple no-ops, literal DISPLAY and bounded literal MOVE stores into validated local scalar fields. Stores require complete ordinary source and unaliased storage. Source-mode barriers, ALTER, unresolved targets, cycles, fallthrough and other statement effects prevent that jump proof. Preserve the existing path and describe it in the value evidence. 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. A jump path may also end in exactly EXEC CICS RETURN END-EXEC with no options. Validate the complete embedded command and retain the existing path budgets and source barriers. This exits the current CICS logical level. It does not establish that the whole task terminates. Commands with response, routing, data-passing or activity options remain outside this proof. Preserve the original return command and report its actual source line. 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. Also permit bounded default INITIALIZE on these terminal jump paths. Validate at most 16 local fields or groups and 64 elementary writes. Require complete ordinary unaliased storage. Integer defaults are zero and PIC X defaults are spaces within 256 characters per field. VALUE and FILLER phrases, replacement phrases, FILLER members, tables and unsupported storage prevent this proof. An explicit TO DEFAULT retains default behavior. Preserve every initialization and message before the existing terminal. Preserve a separately established local forwarding length across a terminal received-count guard. Require a complete read-only count condition, fully known arrivals and at least one admitted continuing count. Retain the existing storage checks, terminal-exit proof and 64-step scalar evidence budget. Empty or unknown entry sets, unsupported branches and unmodeled native counts cannot establish this preservation. 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.