Analyze COBOL table access bounds

Resolve each COBOL table reference to its OCCURS dimensions and compare integer literal subscripts with the declared bounds. Infer nominal counter ranges for literal TEST BEFORE VARYING loops with one non-mutating MOVE and a fixed one-dimensional table. Report other dynamic subscripts and unresolved declarations explicitly. Propagate representable integer MOVEs, supported LENGTH OF assignments and single literal ADDs for simple MOVE accesses and bounded UNSTRING destinations. Join top-level sentences only in programs without NEXT SENTENCE or procedural COPY. Paragraph and section boundaries reset facts. The UNSTRING proof requires one receiving field, an ordinary text sender and a literal delimiter. It excludes auxiliary writes and overflow handlers. LENGTH OF supports ordinary PIC X fields and fixed DISPLAY groups of PIC X and unsigned PIC 9 fields. Group layouts are bounded to 32767 bytes and must be complete. Also propagate direct MOVE or COMPUTE assignments of FUNCTION LENGTH for ordinary fixed PIC X fields. COMPUTE must have one target and no arithmetic, rounding or size-error handlers. This length is field capacity, not received payload size. Retain exact values after bounded IF branches when both paths agree. Conditions must be plain numeric or character comparisons, or level-88 tests. Other effects and control-flow boundaries stop this local proof. Produces tables without marking or changing source. Values within an OCCURS DEPENDING ON maximum still require validation against the current count. Does not analyze opaque EXEC operands or prove reachability. Also accept AND, OR, NOT and parentheses when every condition term is supported. Limit each condition to 64 atomic terms and 16 levels of parentheses. Abbreviated relations and unknown terms remain unresolved. 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 retain sets of at most 16 integer candidates across supported IF branches, copies and literal additions. A set proves a bounds violation only when every candidate is outside the dimension. Mixed sets remain unproven because branch unions can include infeasible values. Report the candidates and their minimum and maximum. Do not treat the interval between candidates as observed values. 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. Literal TEST BEFORE loops may use any nonzero integer step in the direction of the supported stopping inequality. Calculate the last value actually visited and require the terminating increment to fit the counter. Do not treat skipped values near the threshold as visited subscripts. Complete unrelated REDEFINES records do not prevent local numeric proofs. Both redefined records are excluded in full. Writes through excluded storage clear incoming values. RENAMES and unresolved alias relationships remain barriers. 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.