Find TSQ writes that exceed their source areas

Compare literal or exactly established local WRITEQ TS lengths with their source areas. Prove excess reads for standalone PIC X items and whole DISPLAY records in ordinary working or local storage. The requested length must be within the command's supported positive range. Local lengths require ordinary signed halfword binary storage and a complete command with plain operands. Response and item outputs require supported binary fields and cannot share the length field. Earlier EXEC islands and unknown effects invalidate local facts. Record inferred lengths and assignment evidence. Record fields may be PIC X or unsigned DISPLAY PIC 9 integers. Layouts must be exact and at most 32767 bytes. Slices, tables, aliases, linkage, external storage and incomplete layouts require further analysis. Report evidence and the missing contract for remediation. The analysis does not prove reachability or infer the intended record length. Also summarize a noniterative PERFORM of one uniquely resolved paragraph. Allow explicit IN or OF section qualifiers. Limit the expanded call tree and all branches to 64 statements. Follow at most 16 active local paragraphs. Reject recursion and unresolved targets. Count repeated invocations separately. Supported IF and EVALUATE branches retain every alternative. Conditions count toward the statement limit. Limit combined caller and callee condition nesting to 16. Ranges, sections, CALL statements, control transfers and procedural COPY prevent that summary. Also resolve direct LENGTH OF operands for supported fixed DISPLAY declarations. This proves storage size rather than payload length. It does not require an assignment or reuse stale command-entry facts. Also evaluate direct LENGTH(TRIM(field TRAILING)) assignments when the fixed PIC X contents are locally proven. Only spaces at the end are removed. Leading spaces remain and an all-space input gives zero. The resulting character count does not establish transport length, general whitespace validity or permission to trim input. Other trim modes, unknown contents and unsupported expressions remain unresolved. Also join supported EVALUATE branches without selecting a path. Integer selectors allow literal values and ranges. Character selectors allow character literals. TRUE and FALSE selectors use supported read-only conditions. Include the incoming state when WHEN OTHER is absent. Limit selection to 64 WHEN labels and combined IF and EVALUATE nesting to 16 levels. Unknown effects invalidate the join. Table checks retain at most 16 candidates. Reference and TSQ lengths still require every retained candidate to agree. Simple EXIT and CONTINUE preserve local facts. 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. Propagate a single integer literal SUBTRACT FROM one supported integer field of at most 18 digits. The literal also has at most 18 digits. Discard the fact if any result does not fit the receiving picture. Multiple operands, GIVING, CORRESPONDING, rounding and size-error clauses remain unsupported. Assign the first declared integer value for supported SET condition-name TO TRUE statements. Numeric range declarations assign their lower endpoint. Supported character assignments preserve unrelated integer facts. Validate every declaration and target before applying assignments from left to right. Limit each SET to 16 condition names and each declaration to 64 value intervals. Unsupported forms discard local facts. Model plain INITIALIZE of at most 16 ordinary fields or groups. Validate every member before applying at most 64 elementary writes. Supported integers become zero and PIC X fields of at most 256 characters become spaces. Declaration VALUE clauses do not supply these values. Preserve unrelated local values. FILLER members, OCCURS, replacement phrases and unsupported storage prevent this proof. Validate STRING DELIMITED BY SIZE with at most 16 nonoverlapping ASCII literal or ordinary PIC X sources and a receiver of at most 256 characters. Require all transfers to fit without a pointer or overflow handler. Preserve unrelated local facts. Construct character values only from known sources and retain the previous unwritten suffix. An unknown suffix remains unknown. Bound character sets to 16 values and evidence to 64 steps. 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. 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. 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.