Find failed COBOL checks falling through to protected calls

Find a failed check that falls through to a protected literal CALL. The approved contract names the level-88 success condition and protected routine. The proof covers a selected failure branch followed by the protected call in the same statement sequence. 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. Between the check and call, the proof also accepts literal assignments and equal-width ordinary text copies that preserve the failed condition. The call may have no arguments or plain BY REFERENCE arguments. Other branch effects, incomplete source and unresolved storage require further analysis. The analysis does not follow general subroutine flow or jumps. It does not prove reachability or infer authorization policy or failure exits. 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.