facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.89k stars 2.01k forks source link

How do I check all the summaries of procedures? #1682

Open sujin0529 opened 1 year ago

sujin0529 commented 1 year ago

Please make sure your issue is not addressed in the FAQ.

Please include the following information:

I analzed the following 'Main.java' file.

class State {
    public void execute() {

    }
}

class Obj {
    public State getState(int i) {
        if (i == 0)
                return new State();
        else
                return null;
    }
}

public class Main {
    public void f(Obj o, int i) {
        State s = o.getState(i);
        s.execute(); // NPE
    }
}

And when I checked the procedure-summary, I got the following output. (The code below is part of the output.)

void void Main.f(Obj,int)(Main* this, Obj* o, int i)
Analyzed
ERRORS: Null Dereference
WARNINGS:
FAILURE:NONE SYMOPS:44
Biabduction: phase= RE_EXECUTION
--------------------------- 1 of 1 [nvisited:17 18 19 20] ---------------------------
PRE:
i = 0:; this = val$2:; o = val$1: ;
o|->{}:
POST 1 of 1:
i = 0:; return = val$3:; this = val$2:; o = val$1: ;
o|->{}:

In the above output, I don't understand why only 'i = 0' condition is included in the precondition and postcondition. (why 'i != 0' condition is not included in procedure f summary?)

Based on the output, I think that if an error occurs, the procedure-summary is removed from the original procedure summary. Am I right? Then, how do I see the procedure-summary for the precondition and postcondition with errors?

Thanks.