|
|
|
/*
|
|
|
|
* Copyright (c) 2015-present, Facebook, Inc.
|
|
|
|
*
|
|
|
|
* This source code is licensed under the MIT license found in the
|
|
|
|
* LICENSE file in the root directory of this source tree.
|
|
|
|
*/
|
|
|
|
|
|
|
|
package codetoanalyze.java.tracing;
|
|
|
|
|
|
|
|
import com.facebook.infer.annotation.Verify;
|
|
|
|
|
|
|
|
public class NullPointerExceptionExample {
|
|
|
|
|
|
|
|
void deref(T2 t) {
|
|
|
|
t.f();
|
|
|
|
}
|
|
|
|
|
|
|
|
@Verify
|
|
|
|
void callDeref(T2 t, boolean condition) {
|
|
|
|
if (condition) {
|
|
|
|
deref(t);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
report errors when all the postconditions are error states
Summary:
The philosophy of the tracing mode reporting is to not report the errors in a method if reaching this error does depend on information that can be false at call site. Typically with:
void foo(Object obj, int x) {
if (x == 3) {
obj.toString();
}
}
it may be that we always call `foo` with a non-null parameter or `x != 3`.
Thechnically, the reporting code matches the pairs of the form (precondition, error) and filtering out the cases where the precondtions was not imposing constraints on the calling context, and report the other cases. So the NPE could be reported in the following case:
void bar() {
foo(null, 3);
}
However, we were missing the case where there was anyway no way to call a method in a safe way, i.e. all the preconditions were of the form: (precondition, error), for example:
void baz(boolean b) {
if (b) {
foo(null, 3);
} else {
foo(null, 3);
}
}
In that case, the summary is of the form
PRE (1): b = false
POST: NullPointerException
PRE (2): b = true
POST: NullPointerException
In which case it is legit to report `NullPointerException` in `baz`.
Reviewed By: sblackshear, jberdine
Differential Revision: D3220501
fb-gh-sync-id: 7fb7d70
fbshipit-source-id: 7fb7d70
9 years ago
|
|
|
void callDoesNotLeadToNpe() {
|
|
|
|
callDeref(null, false);
|
|
|
|
}
|
|
|
|
|
|
|
|
void callLeadToNpe() {
|
|
|
|
callDeref(null, true);
|
|
|
|
}
|
|
|
|
|
|
|
|
void npeOnBothBranches(int x) {
|
|
|
|
if (x < 2) {
|
|
|
|
callDeref(null, x < 3);
|
|
|
|
} else {
|
|
|
|
callDeref(null, true);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
}
|