You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
|
|
/*
|
|
|
|
* Copyright (c) 2015 - present Facebook, Inc.
|
|
|
|
* All rights reserved.
|
|
|
|
*
|
|
|
|
* This source code is licensed under the BSD style license found in the
|
|
|
|
* LICENSE file in the root directory of this source tree. An additional grant
|
|
|
|
* of patent rights can be found in the PATENTS file in the same directory.
|
|
|
|
*/
|
|
|
|
|
|
|
|
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);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
}
|