Skip translator-rejected methods gracefully and support char primitive

[fabiomadge]

Step 1 of the JVerify completion plan (PLAN.md §3.1).

Resolves

• Laurel compiler: Graceful skip of unsupported methods (catch JavaViolationException) #398 — graceful skip of unsupported methods (catch JavaViolationException)
• Laurel compiler: char primitive type support #414 — char primitive support

Summary

• Wrap per-method translation in JavaToLaurelCompiler.visitMethodDef in a try/catch on JavaViolationException. On catch: emit a translatorError diagnostic and demote the method's IntervalTree entry from Verified to Skipped.
• The trailing super.visitMethodDef stays outside the catch so nested classes are still visited even when the parent method skipped.
• Catch scope is narrow — JavaViolationException only. Broader catches would mask translator bugs (NPEs, "Could not find line map for...") and OOM/StackOverflow from Strata recursion.
• Add char as a constrained int (0..65535, full UTF-16 range) registered alongside int8/int16/int32/int64.

Why bundle char with #398

5-line type-plumbing tweak — too small for its own step. Mechanically aligned with the safety-net edits (both touch translateType / convertLiteral), and unblocks Step 2's switchExprChar/switchExprCharBad and Step 5's char-using methods in PrimitiveTypes without leaving them gated on a follow-up.

Implementation notes

• VerifyAnnotationCompiler.markSkipped(JCCompilationUnit, JCMethodDecl) — new helper. Scans the URI's interval-tree by methodTree == methodDecl identity rather than recomputing line position, so it doesn't depend on PositionCalculator semantics matching addMethodToIntervalTree exactly. No-op when the method has no entry (synthetic methods, methods without an implementation body) — those are already invisible to the counting layer.
• Strata has no char/char16 prelude type (verified via grep of Strata/Languages/Laurel/); inlining as a constrained int is the only path. Dafny used a named char16 type — a forced divergence.
• translatorError (new messages.properties key) instead of notSupported. JavaViolationException's javadoc states "Indicates a JVerify compiler bug" — so it's a translator gap surfaced to the user, not a clean refusal of an explicitly-unsupported feature. Future Step 6 throws → reportError migrations will use notSupported for the genuine "user feature not supported" cases.

Test plan

• ./gradlew :verifier:test passes — 113 tests / 0 failed / 72 skipped.
• No new uncaught JavaViolationException stack traces in test output.
• No test transitions green → red.
• TranslatorSkip.java covers the catch wrapper end-to-end. Asserts three properties simultaneously: (1) sibling translation continues past a throwing method, (2) the translator-level error reaches the driver as a diagnostic, (3) the throwing method's status flips Verified → Skipped (the silent-overcount bug §3.1 calls out). Trigger is the multi-init for refusal at convertStatement, chosen for stability — the plan refuses this form rather than supporting it.
• CharPrimitive.java is the regression test for Laurel compiler: char primitive type support #414. Pairs the happy path (translateType + convertLiteral round-trip) with rangeBoundsBad that fails when c == 65535 to assert the 0..65535 constraint is actually enforced rather than dropped.

[keyboardDrummer]

Interesting! I have trouble evaluating the UX but it seems great. Would JVerify previously just crash if it ran into something that was not supported?

[keyboardDrummer]

Nice!