Infer: eradicate and try-catch

[pontusbostrom]

It seems that infer: eradicate treats catch-blocks as never executed, at least in some cases. Below is an example class that "infer -a eradicate" claims has no issues. If the assignment "path = null" is moved after the catch-block (or into the try-block) then the assignment "filePath = path" is (correctly) flagged as an error. Is this a bug in infer or an issue with models?

public class ExceptionTest {
    String filePath = "";
    public OutputStream returnStream(){
        File file = null;
        OutputStream stream = null;
        String path = null;
        try{
            file = File.createTempFile("tmp", "tmp");
            stream = new FileOutputStream(file);
            path = file.getAbsolutePath();
        }catch(IOException e) {
            path = null;
        }
        filePath = path;
        return stream;
    }
}

[cristianoc]

Thanks for the report. It seems to be a library modelling issue, as calling a locally defined method declared as throwing IOException causes the expected error to be reported.
Stay tuned.

[cristianoc]

Currently Infer does not analyze the jar of the standard library to get information on declared exceptions.
Turning to wishlist.

[pontusbostrom]

Thank you for your reply, and good to know this is on the wishlist. As a workaround, I tried to add a model of the method with the correct throws clause. However, it seems that adding a model that throws exceptions doesn't help in this case. Is this also not supported yet?

[cristianoc]

Eradicate uses a different modeling mechanism than the core Infer analysis, with tables for annotations instead of actual code, as the implementation of called methods is not used by Eradicate's analysis.
It would be easy to add tables for exceptions as well, as a temporary solution while the full solution is being developed.