Treat results of methods without refinements as unconstrained in operations

[CatarinaGamboa]

When an invocation of a method with no refinements (e.g. s.length(), s.equals(..), list.size()) was an operand of a comparison or boolean operator, OperationsChecker looked up the RefinedFunction, got null, and crashed with an NPE, even in programs with no refinements at all.

Now, in both getOperationRefinements (invocation branch) and getOperationRefinementFromExternalLib, a missing function yields a fresh variable of the invocation's type with refinement true, so the result is treated as unconstrained instead of breaking verification.

Fixes #300

Testing

• New CorrectUnknownMethodInComparison: if (s.length() < 3), s.equals("a") || s.equals("b"), and a for loop bounded by list.size() (crashes without the fix).
• New ErrorUnknownMethodInOperation: @Refinement("_ > 0") int x = s.length() + 1; is still reported as a Refinement Error (no information is assumed about the result).
• mvn test: 340 tests run, 0 failures, 0 errors.
• The repro from the issue now prints Correct! Passed Verification. via ./liquidjava.

🤖 Generated with Claude Code

[CatarinaGamboa]

Review of the fix, plus a follow-up commit (b7ad615).

Checked

• Unknown method result inside a condition: the fresh variable has no constraints, so both the then and else branches are still checked. Violations in either branch are reported.
• Typestate: calling a method without a spec on an object that does have a state spec (for example if (r.count() > 0)) leaves its state unchanged, and a later wrong state is still reported. The skipped this substitution in getOperationRefinementFromExternalLib only rewrites the return refinement, which is empty here. I also checked the external-lib path by hand with an InputStreamReader spec and isr.ready() after close(): read() is still flagged.
• Types: list.get(0) > 3 (boxed Integer), l.get(0) > 1.5 (Double) and map.containsKey(k) && n > 0 (boolean) work fine with inv.getType().

Problems found and fixed

1. In getOperationRefinementFromExternalLib, a call whose target is not a variable (chained s.trim().length() > 0, static Math.max(a, b) > 0) still returned new Predicate() (true). The operation became true > 0, and Z3 crashed with BoolExpr cannot be cast to ArithExpr. It now returns getUnconstrainedInvocationVariable(inv) too.
2. A method declared in an interface (if (shape.area() > 0)) crashed with a ClassCastException on (CtClass<?>) method.getParent(). It now uses method.getParent(CtType.class).

Tests (positive and negative now mirror each other)

• CorrectUnknownMethodInComparison: extended with both branches, boxed result, boolean &&, static call, chained call, implicit-this call and interface method.
• ErrorUnknownMethodInComparison (new): the same shapes, each with a violation inside the branch that must still be flagged. The verifier stops at the first error in a method, so there is one error per method.
• CorrectUnknownMethodInComparisonState / ErrorUnknownMethodInComparisonState (new): typestate is kept across an unknown call in a condition.
• ErrorUnknownMethodInOperation: unchanged.

On the original PR code, both new Correct and Error files crash (interface cast). With the fix, mvn test gives 343 tests, 0 failures.

🤖 Generated with Claude Code