Analyze failed numeric COBOL checks before protected paragraphs

Find a numeric failure check that falls through to a protected local PERFORM. The approved contract names the result field, every accepted integer value, and one unique local paragraph in one source and program. A level-88 declaration is not required. The selected IF branch must exclude every accepted value and admit a representable failing value. Select a failure THEN branch or an explicit failure ELSE branch. Effects in the other branch do not establish the selected path. An absent ELSE is not analyzed as an implicit failure path. Failure branches may use CONTINUE, simple EXIT, plain literal DISPLAY, supported disjoint assignments or a proven returning local message paragraph. A message paragraph may contain read-only IF or EVALUATE branches with supported assignments, bounded message construction, plain literal DISPLAY, CONTINUE or simple EXIT at every leaf. Allow nested noniterative single-paragraph PERFORM with explicit IN or OF section qualifiers. Limit the expanded call tree to 64 statements, 16 active paragraphs and 16 levels of conditions. Recursion, CALL, control transfers and unknown effects prevent the proof. A PERFORM between the completed check and the protected operation remains a barrier. Intervening literal assignments and equal-width text copies must preserve the result field. Only a plain noniterative PERFORM of that paragraph is supported. Its later effects are not inferred. Support full integer comparisons, AND before OR, NOT and parentheses. Limit conditions to 64 terms and 16 levels of parentheses. Unknown effects, other fields, arithmetic, functions, abbreviated conditions, aliases and incomplete source prevent findings. The analysis does not prove reachability, result provenance, accepted SQL or CICS codes, or an appropriate failure exit. Report the missing failure-path contract without changing application behavior. Also analyze EVALUATE of the configured field with up to 64 integer literal WHEN labels or inclusive ranges. Honor first-match order, shared branch bodies, WHEN OTHER and an implicit no-match path. Require every accepted value to select another branch and a representable failing value to select the reported branch. The selected body and intervening assignments must preserve the result field. Unsupported selectors or labels prevent selection proofs. 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. Failure messages may SET condition names TO TRUE when every parent field is disjoint from the checked field. Validate all targets and complete value clauses before accepting the statement. Retain the existing 16-target and 64-value limits. Changes to the checked field remain barriers even when assigning a failing value. Supported intervening SET statements preserve the failed result and count as assignment statements. Also permit plain INITIALIZE of disjoint error or request fields. Validate at most 16 targets and 64 elementary writes using the declared storage. Every initialized field must be disjoint from the checked result. Initialization never establishes a successful check. Allow the same initialization inside bounded returning message paragraphs. Supported intervening initialization counts as an assignment. FILLER, OCCURS, replacement phrases, unsupported storage and any write to the checked result prevent this proof. Permit bounded STRING DELIMITED BY SIZE into ordinary PIC X storage disjoint from the checked value. Validate every operand and require the complete write to fit the receiver. Limit operands to 16 and fields to 256 characters. Overlap, pointers, overflow handlers and unsupported forms remain barriers. Allow these messages in the failure branch and bounded returning message paragraphs. Constructing a message does not reject the failed operation. Supported intervening STRING preserves the failed result and counts as an assignment statement. 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.