|
|
|
/*
|
|
|
|
* Copyright (c) 2013 - 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 endtoend.c;
|
|
|
|
|
|
|
|
import static org.hamcrest.MatcherAssert.assertThat;
|
|
|
|
import static utils.matchers.ResultContainsExactly.containsExactly;
|
|
|
|
|
|
|
|
import org.junit.BeforeClass;
|
|
|
|
import org.junit.Test;
|
|
|
|
|
|
|
|
import java.io.IOException;
|
|
|
|
|
|
|
|
import utils.InferException;
|
|
|
|
import utils.InferResults;
|
|
|
|
|
|
|
|
public class AssertionFailureTest {
|
|
|
|
|
|
|
|
public static final String SOURCE_FILE =
|
|
|
|
"assertions/assertion_failure.c";
|
|
|
|
|
|
|
|
public static final String ASSERTION_FAILURE = "ASSERTION_FAILURE";
|
|
|
|
|
|
|
|
private static InferResults inferResults;
|
|
|
|
|
|
|
|
@BeforeClass
|
|
|
|
public static void runInfer() throws InterruptedException, IOException {
|
|
|
|
inferResults = InferResults.loadCInferResults(AssertionFailureTest.class, SOURCE_FILE);
|
|
|
|
}
|
|
|
|
|
|
|
|
@Test
|
|
|
|
public void whenRunsOnAssertionFailureThenAssertionFailureIsFound()
|
|
|
|
throws InterruptedException, IOException, InferException {
|
|
|
|
String[] methods = {
|
|
|
|
"simple_assertion_failure",
|
|
|
|
"should_report_assertion_failure",
|
|
|
|
"assertion_failure_with_heap",
|
|
|
|
"assignemt_before_check",
|
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
|
|
|
"failure_on_both_branches",
|
|
|
|
};
|
|
|
|
assertThat(
|
|
|
|
"Results should contain " + ASSERTION_FAILURE,
|
|
|
|
inferResults,
|
|
|
|
containsExactly(
|
|
|
|
ASSERTION_FAILURE,
|
|
|
|
SOURCE_FILE,
|
|
|
|
methods
|
|
|
|
)
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
}
|