Find locally established CALL targets outside an approved policy

Compare bounded local character sets at dynamic CALLs with an explicit approved field policy. A finding requires every established value to be outside that policy. Mixed sets remain unproven because branch unions can include infeasible values. Use literal MOVEs, equal-width PIC X copies and bounded IF joins with plain comparisons or level-88 conditions. Calls and unknown effects stop propagation. Paragraph and section boundaries reset facts. Preserve facts across disjoint numeric literal MOVEs. Exclude whole redefined records while allowing unrelated storage. Join top-level sentences only in programs without NEXT SENTENCE or procedural COPY. Do not infer entry values, reachability, compiler name mapping or external control. Do not select a replacement target or failure path. Report a policy violation without assigning a CWE that needs further evidence. 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 join supported EVALUATE branches without choosing a path. Integer selectors allow literal values and ranges. Character selectors allow character literals. TRUE and FALSE selectors use supported read-only conditions. An absent WHEN OTHER includes the incoming state. Unknown alternatives discard the affected value set. Retain case and padding. Limit selection to 64 WHEN labels, combined branch nesting to 16 levels, sets to 16 values and evidence to 64 steps. 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. Assign the first declared character value for supported SET condition-name TO TRUE statements. Pad supported PIC X fields to their declared width of at most 256 characters. Supported numeric assignments preserve unrelated character 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 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.