How do I use Coverity modelling to mark a method as non-returning?

Question

I am using the free Coverity Scan service for a learning project and I would like to model a few methods as either always throwing exceptions, or calling internally System.exit(), hence non-returning, in order to get better results from Coverity's flow analysis.

For example:

class Foo {
    // given these
    Blarg fieldFromTheClass

    void fail(String s, int a, int b) {
        throw new DomainSpecificBlahBlahException(s, someFunction(a), someOtherFunction(a, b), fieldFromTheClass, collaborator.getBaz());
    }

    void fatal(Strin s) {
        System.out.println("Fatal error: " + s);
        System.exit(1);
    }

    // we should get 2 flags here
    void test(int i) {
        if (i%2==0) {
            try {
                fatal("foobar");
            } catch (SecurityException se) { 
                // recovering from security manager - should be flagged as unreachable in normal circumstances
            }
        } else {
            fail("baz", 1, 3);
        }

        doSomethingElse(); // unreachable
    }
}

What would be the way to do that with a modelling file?

Also, are the Coverity annotations available in any public repository (i.e. Bintray or Central)?

Answer 1

Coverity is supposed to automatically figure out which functions exit or never return for some reason, but it does indeed seem to miss some. In that case, you can model the functions and that model would look something like this:

#ifdef __COVERITY__
void fatal(String s) {
    __coverity_panic__();
}
#else
// real definition of fatal

There should be some examples in (coverity_installation)/library.