Summary:
This also adds `-a compile` support to `InferClang`. This is needed for the
`xcodebuild` integration, which is hard to fold into the same binary as the
rest.
Reviewed By: jberdine
Differential Revision: D4008262
fbshipit-source-id: 0bbd53f
Summary:
This diff fixes two issues in the backend that were causing Bad_footprint
errors when abducing pointsto facts for expressions that start in an array
access and follow up with another structured access, eg `x[0].some_field`:
1. array accesses were assumed to come last in these expressions
2. the type of the root exp passed to the function that walks down the list of
offsets to apply to it was wrong in the case of arrays: it was always the
type of the whole expression instead of the root expr (eg the type of
`x[0].some_field` instead of the type of `x`).
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D3800566
fbshipit-source-id: 0511604
Summary:
Infer doesn't go looking into field values when looking for unsigned
expressions, which could cause some unintended reports.
Reviewed By: sblackshear
Differential Revision: D3724232
fbshipit-source-id: 9c4cd97
Summary:
Call infer with `--unsafe-malloc` or set `unsafe-malloc: true,` in .inferconfig to
have infer assume that `malloc()` never returns null.
closes#389
Reviewed By: jberdine
Differential Revision: D3522169
fbshipit-source-id: 6b88a16
Summary:
The extra dereference in stmtexpr was wrong. When a dereference is needed, we have a cast.
This was causing one dereference too many, and creating wrong results.
Reviewed By: akotulski
Differential Revision: D3393294
fbshipit-source-id: 7a1ec8e
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
Summary:public
When a conditional is the last instruction, there will be a join node leading directly to the exit node.
Some instructions, such as nullification of dead variables, and abstraction, are added to the control flow graph automatically. But, join nodes cannot contain instructions. So when a procedure ends with a conditional, there might be no place to store these instructions.
This diff adds one extra node between the join and the exit node in that situation.
Reviewed By: jvillard
Differential Revision: D3179056
fb-gh-sync-id: 2b9cd7e
fbshipit-source-id: 2b9cd7e
Summary:
public
otherwise Infer cannot know the type of the temporary variable
Reviewed By: dulmarod
Differential Revision: D2845054
fb-gh-sync-id: cf5fb8d
Summary:
public
This diff cleans up the detection of assertion failures in C, C++ and Objective C which was previously hacked on top of the tracing mode for Java. The code is also generalized to detect any custom errors which can be defined using the `__infer_fail` builtin, and the case of assertion failure is now just the specific case of translating `assert` using `__infer_fail` directly in the clang frontend.
Reviewed By: jberdine
Differential Revision: D2786574
fb-gh-sync-id: dd1e1cf
Summary:
public
Lines other than the first of multi-line comments in non-ocaml files
were flush right instead of aligned.
Reviewed By: jvillard
Differential Revision: D2739752
fb-gh-sync-id: c85f56e
Summary: public Buck prints all the output at once and it doesn't look good. So we should not print the progress bar in the tests.
Reviewed By: jvillard
Differential Revision: D2631722
fb-gh-sync-id: 5460a70
Summary:
The symbolic execution was not stopping in case an unitialized dangling pointer was
passed to a function and then dereferenced inside the callee.
What would happen is that a wrong footprint would be added to the unititialized pointer
at the end of the function call in the caller proposition.
This checks that if we do:
frame * new_footprint
checks that we do not add heap predicates to the frame into uninitialized local variables.
If we can identify the variable then we raise a danglind pointer dereference. If instead
we cannot give a good explanation we give an internal error.
The latter case should be temporary. We should find a general way to raise dangling pointer
deref instead of the internal error.
I also fixed the model of getc that was the way I found the problem.
Summary:
This adds a sentinel check every time a function carrying a sentinel attribute
is called, regardless of whether we have a definition for that function or not.
Summary: @publicThe first argument of builtin calls in C gets translated twice, which is bad if the argument is a side-effecting expression like a function call.
Test Plan: Attached test previously reported a memory leak because the translation introduces an extra call to malloc(), now reports nothing.
Summary:
@public
Sorting the fields in structs and classes. Was needed in the backend and forgotten.
Fixes the github issue https://github.com/facebook/infer/issues/90.
Test Plan: Added a new test that shows that we now get a spec for the example from the github issue.
Josh Berdine
Jules Villard
Andrzej Kotulski
Cristiano Calcagno
Sam Blackshear
Dulma Churchill
Dino Distefano
Jeremy Dubreil
Open Source Synchronization