Analyze failed COBOL checks falling through to protected paragraphs

Find a failed level-88 check followed by a noniterative PERFORM of one protected local paragraph. An explicit contract must require the success condition at every entry to that paragraph. Resolve the configured name uniquely within the program. The call can use an explicit IN or OF section qualifier. Section targets, ranges and iteration remain unsupported. 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 failed condition. Other effects, incomplete source, procedural COPY and unresolved storage stop the proof. The finding establishes a violated paragraph entry condition if the failed branch completes. It does not infer the paragraph's effects, prove reachability, invent policy or choose a failure exit. Also recognize pure numeric checks over the condition's parent field when they exclude every declared level-88 value or range. Require integer condition values and ordinary integer storage. Honor AND before OR, NOT and parentheses. Require a representable failing value and record it as evidence. This does not prove that execution reaches the branch. Limit the proof to 64 declared intervals, 64 condition terms and 16 levels of parentheses. Abbreviated comparisons, arithmetic, functions, other fields and unsupported declarations remain unresolved. 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.