Repository navigation
equivalence: cases for GenApp's front-end and test programs (#4270) - #4653
Merged
Merged
Conversation
Eleven GenApp programs whose only proof gap was 'no case': - the front ends LGACUS01, LGAPOL01, LGDPOL01, LGICUS01, LGIPOL01, LGUCUS01, LGUPOL01, each running its whole back-end chain (Db2 service, VSAM service, LGSTSQ) in the task, with the back-end cases' inputs plus the front end's own paths (no COMMAREA, short COMMAREA, wrong request id); - the BMS test transactions LGTESTP1-4 (SSMAP maps, twelve programs per task): inquire / add / delete / update, CLEAR, PF3, MAPFAIL, bad option. Harness / translator fixes, each with a test: - stage_copybooks no longer stages a .bms map source as <NAME>.cpy (it shadowed the generated symbolic map COPY SSMAP means); - a program with no DFHCOMMAREA still gets EIBCALEN from the task's area (LGTESTP's IF EIBCALEN > 0 GO TO A-GAIN); - an integer literal compared with an alphanumeric item keeps its digits as written (ENP4CNOO Not = 0000000000); - each LINKed SQL program's GG-SQL-IDs start at the next free hundred (1000 x its place ran past PIC 9(4) at the tenth program); - ggsql.c refuses a statement the CLI fails in the client (-99999, Q10). LGTESTP4's successful add is left out: #4652 (C11). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…-end cases (#4270) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
squid-protocol
force-pushed
the
equiv/4270-genapp-front-ends
branch
from
October 8, 2026 00:59
cacc05b to
f5f9ecd
Compare
Contributor
squid-protocol
marked this pull request as ready for review
October 8, 2026 14:33
squid-protocol
added a commit
that referenced
this pull request
Oct 8, 2026
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
squid-protocol
added a commit
that referenced
this pull request
Oct 8, 2026
Main's #4653 Lit.digits and #4665's NumLit both pass a numeric literal compared with a nonnumeric item as its characters. Measured against cobc 3.1.2 -std=ibm (IF and EVALUATE): unsigned integer literals as written agree on both; a signed literal is compared with its sign character ('12' is not +12/-12, '+12' is +12, '-12' is -12), which main's sign-stripping digits got wrong and IBM differs on (C13: refused); a decimal literal against an alphanumeric item is its digits as written ('012' = 0.12, which main got wrong). Kept NumLit/literal_text as the one path and dropped Lit.digits. New measurement: a numeric-edited item compared for equality with a literal of more decimal places than its own is decided by cobc when it compiles (ZZ9 holding 125: not = 12.5, NOT = 12.5, yet neither < nor >), so that shape is refused by name too (C13); IBM rejects the non-integer. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of #4270.
Equivalence cases for the 11 GenApp programs whose only proof gap was "no case" (proof_blockers on b8e6430). All 11 prove (local det sweep with Db2,
proof_sweep.py --det-only: 11/11, "as expected"); ledger entries added, evidence report refreshed.The committed report still shows L1 for these programs. They are Db2 cases, which CI's det-sweep skips, so this matches the other GenApp Db2 cases. proof_blockers with the sweep: every one of the 11 moves from "no case" to "coverage: branch outcomes no scenario runs" (plus "live paragraphs" for LGTESTP*).
Cases. Each front end runs its whole back-end chain in one task through
"programs": the Db2 service, the VSAM service and LGSTSQ. It reuses the back-end case's inputs and adds its own paths: no COMMAREA, a short COMMAREA, a wrong or unknown request id, and a failing back end. LGTESTP1-4 run 12 programs per task with the SSMAP BMS maps. Their scenarios cover inquire, add, delete, inquire-then-update, CLEAR, PF3, MAPFAIL and an invalid option, and LGTESTP4 also has its four kinds of inquiry.Uncovered, and why. Every program's WRITE-ERROR-MESSAGE
IF EIBCALEN > 0arm is dead in practice, because the paragraph only runs when EIBCALEN is 0. In LGACUS01 and LGICUS01, the'98'short-COMMAREA branch can't be reached without first writing past EIBCALEN:MOVE '00' TO CA-NUM-POLICIESwrites bytes 91-93 before the check runs (X23). The remaining gaps sit after a back-end failure. Those paths all LINK LGSTSQ first, so they are judged only up to its refused WRITEQ (X6): LGDPOL01 line 127, and NO-ADD / NO-DELETE / NO-UPD in LGTESTP*.Harness / translator fixes (each with a test):
stage_copybooksno longer stages a.bmsmap source as<NAME>.cpy. GenApp'sssmap.bmswas hiding the generated symbolic map thatCOPY SSMAPrefers to.IF EIBCALEN > 0 GO TO A-GAINwent the wrong way.ENP4CNOO Not = 0000000000, the Java side was comparing against"0".ggsql.cnow refuses, by name, a statement the Db2 CLI fails in the client (its own native code -99999; the JDBC side gives -4220). This is oracle_assumptions Q10.Left out: LGTESTP4's successful add. Its CA-BROKERID / CA-PAYMENT fields are space-filled and moved to binary (GnuCOBOL 931773840, det port 0; C11), filed as #4652.
Note: this changes the harness and oracle fingerprints, so existing ledger entries go stale-warn until the next scheduled refresh. #4647 also touches equivalence_cics.py; whichever PR lands second rebases.
🤖 Generated with Claude Code