GeezerVison

Closes #339 and #364.

try/catch was checked as straight-line code: first the try, then the catch. An exception can leave the try after any statement, and a finally also runs after returns and uncaught exceptions. Because of that, errors in all three places were missed.

Example

int y = 1;
try {
    y = -1;
    load();               // may throw
    y = 2;
} catch (Exception e) {
    // (1) start of catch
    y = 3;
} finally {
    // (3) start of finally
}
// (2) after the try statement

Walkthrough

1. Start of the catch: while checking the try, every new value of y is recorded (-1, 2). The catch starts from "the value before the try or any recorded value". So @Refinement("_ > 0") int a = y; placed at (1) is now an error; on main it passed.
2. After the try statement: the try and the catch are joined like an if/else on an unknown condition c, reusing the if machinery. So @Refinement("_ == 3") int b = y; placed at (2) is now an error.
3. Start of the finally: it starts from any value seen in the try or the catch. After it, checking continues from the joined state (2), plus whatever the finally assigns.

Path conditions from inside a branch (e.g. if (x <= 0) return; in the try) are also dropped before the next branch, the finally and the code after, since the exception may come before the check.

Changes

• New TryChecker: holds the try/catch/finally logic. The existing try-with-resources code moved there from RefinementTypeChecker, which is now smaller than on main.
• Context: startRecordingInstances / stopRecordingInstances record the new values variables get inside a block.
• Tests: try_catch_error and try_catch_correct, 13 cases each.

Limitations

• A finally that updates a variable from itself (y = y + 1) starts from every possible value. This is sound but imprecise.
• Fields are not tracked, the same as for ifs.
• Catch and finally entries conservatively include the pre-try state even when only later operations can throw. This can reject valid code such as x = 1; risky(); followed by a catch requiring x == 1. Exception-point-aware snapshots would improve precision.

🤖 Generated with Claude Code