Analyze locally established CICS targets outside an approved policy

Compare exact local character sets at a configured CICS routing operation with an approved field policy. Require eight-character program fields or four-character transaction fields. Preserve case and padding. Only a set whose every value is disallowed establishes a finding. Mixed sets remain unproven because branch unions can include infeasible values. Use bounded local MOVEs, copies and read-only IF joins. Unknown effects and earlier EXEC commands invalidate facts. Join ordinary sentences only without NEXT SENTENCE or procedural COPY. Unsupported commands and incomplete source remain unresolved. Do not infer resource-name mapping, external control, authorization or reachability. Do not change the target, failure handling or transaction behavior. 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. LOAD accepts documented ENTRY and FLENGTH options alongside SET and LENGTH. Unsupported option spellings and effects remain unresolved. SYSID is supported for LINK. XCTL with SYSID remains unresolved because that command does not support the option.