GeezerVison

Codex review, round 1

• [P2] Utils.java:190 — replaceAll("\\s+", " ") changes whitespace inside string literals and text blocks. A call such as check("a b") will appear in diagnostics as check("a b"), which is different source code. Collapse whitespace only outside literals, or preserve the source slice as written.

Codex review, round 1: response

• Fixed: whitespace collapsing. Utils.getSourceCode now only joins the lines of a multi-line argument (a line break and the indentation around it become one space), so spacing inside string literals is kept. A text block argument still has its lines joined, which is needed to show it on one line.

Codex review, round 2

• [P2] MethodsFunctionsChecker.java:468 — Distinct calls with identical source text receive the same display name. For example, two next() arguments can be separate values to the verifier but both appear as next() in a failed precondition or counterexample, producing misleading output such as next() < next(). Keep an occurrence marker or instance suffix when the display names collide.

Codex review, round 2: response

• Fixed: calls written alike. The argument now keeps its instance counter like every other instance (size()³ >= 0 is not a subtype of size()³ > 0), so between(next(), next()) shows next()⁴ and next()⁶. The PR description is updated with the new messages.

Codex review, round 3

• [P2] Utils.java:188 — Joining every source line also joins lines inside a Java text block passed to a call. The displayed binder and counterexample can therefore show different text from the argument the caller wrote. Preserve literal contents when formatting the snippet.

Codex review, round 3: response

• Declined: text blocks inside a call argument. Message rows, binders and counterexamples are one line each, so a multi-line argument has to be joined to be shown at all; keeping a text block's line breaks would break the row layout. Only the line breaks change, never the characters on a line, and a text block passed to a refined call inside another call's argument is rare. No code change this round.

Codex review, round 4

Nothing relevant found. The new argument names affect diagnostic formatting only; no change to the verifier's proof obligations and no concrete correctness issue.

Codex review, round 5 (after rebasing on #483 and #484)

• [P2] MethodsFunctionsChecker.java:465 — An invocation argument without a source position can crash verification here. Spoon returns a no-source fragment in that case, so reading its source code is unsafe. Check for a usable fragment and fall back to iArg.toString() for display.

Codex review, round 5: response

• Fixed, differently: a call argument with no source position (one Spoon builds itself rather than reading from a file) is no longer renamed and keeps the parameter name. Falling back to iArg.toString() would print Spoon's form (Basket.count()), which is not what the caller wrote either. Amended into the single commit.