In CFG, unchecked exceptions from method calls should be modeled using RuntimeException | Error rather than Throwable

[msridhar]

Currently, in CFG construction, method calls are modeled as possibly throwing a java.lang.Throwable, corresponding to the possibility of the call throwing an unchecked exception. However, this is imprecise, as Throwable also includes the possibility of throwing a checked Exception. This can lead to infeasible control flow, e.g.:

public void foo(java.net.Socket s) {
    try {
        sock.isClosed();
        sock.close();
    } catch (java.io.IOException e) { }
}

Currently, the Checker Framework CFG adds an exceptional edge from the isClosed() call to the catch block, which is infeasible and can lead to false positives.

Instead, modeling of unchecked exceptions from calls should use two exceptional edges with types RuntimeException and Error, to more precisely capture the possibilities.
This issue was previously discussed (indirectly) in a PR comment on a Checker Framework fork:

opprop#134 (comment)