Summary: Those are not particularly relevant for the biabduction analysis. It would be easy to have a dedicated checker for this if we happen to need one day.
Reviewed By: sblackshear
Differential Revision: D5530834
fbshipit-source-id: 316e60f
Summary: Using a dedicated abstract domain, like Quandary does, is more suitable for taint analysis.
Reviewed By: sblackshear
Differential Revision: D5473794
fbshipit-source-id: c917417
Summary:
Both `stringWithUTF8String` and `stringWithString` implements copy semantics that copies the content of their parameter into a newly allocated buffer. We modeled this as pointer assignment in the past, which means that once we write
```
NSString* foo() {
char buf[...];
...
return [NSString stringWithUTF8String:buf];
}
```
We are going to get a spurious stack variable address escape report because local pointer `buf` is assigned to the newly created string and the string gets returned.
This diff tries to address the issue by heap-allocating a buffer and `memcpy` the contents in `stringWithUTF8String` and `stringWithString`. But this change will create another problem: the allocated buffer will be reported as leaked by the backend, while in reality those buffers won't actually be leaked as they are allocated in a region that will be periodically autoreleased. To suppress spurious memory leak FPs, I added another attribute `Awont_leak` that will suppress the leakage report on any expressions that get tagged with it.
Reviewed By: jeremydubreil
Differential Revision: D5403084
fbshipit-source-id: df6de7f
Summary:
This diff tries to achieve the followings: if we have the following C++ codes:
```
bool foo(int x, int y) {
return &x == &y;
}
```
We want the C++ frontend to emit Sil as if the input is written as
```
bool foo(int x, int y) {
if (&x == &y) return 1; else return 0;
}
```
This matches the behavior of our Java frontend.
The reason why we prefer an explicit branch is that it will force the backend to eagerly produce two different specs for `foo`. Without the explicit branch, for the above example the backend would produce one spec with `return = (&x == &y)` as the post condition, which is not ideal because (1) we don't want local variables to escape to the function summary, and (2) with the knowledge that no two local variables may alias each other, the backend could actually determines that `&x == &y` is always false, emitting a more precise postcondition `return = 0`. This is not possible if we do not eagerly resolve the comparison expression.
Reviewed By: akotulski
Differential Revision: D5260745
fbshipit-source-id: 6bbbf99
Summary:
Adds a new type and branching for a missing path of execution.
closes#575
Reviewed By: jvillard
Differential Revision: D4738681
fbshipit-source-id: f72344c
Summary:
In particular, the method for retrieving an element from the array, this should never be nil. Also added a model for count
similar to the one for NSString length.
Reviewed By: ddino
Differential Revision: D4306655
fbshipit-source-id: 0ecb25a
Summary:
Dealing with symbolic links in project root is tricky. To avoid it, always normalize all paths to sources with `realpath`.
Changes to tests are expected - infer started to resolve symbolic links which screws up with our testing mechanism.
Reviewed By: jberdine
Differential Revision: D4237587
fbshipit-source-id: fe1cb01
Summary:
Run all clang tests with project-root at `infer/tests`. I need it because we'll start resolving symbolic links
soon and some tests would lead outside of project root which means we'd start seeing absolute paths in recorded tests.
Diff that does same thing for java tests: D4233236
Reviewed By: jberdine
Differential Revision: D4233194
fbshipit-source-id: c261a2b
Summary:
Record an abstraction of the bug traces in the tests. The abstraction of a
trace is the sequence of descriptions. In practice, descriptions are either
empty, or of the form "start/end/return from/call to procedure X". They seem
pretty stable.
Motivation: there is nothing testing the traces reported by Infer right now,
even though they are surfaced to developers. For instance, Quandary uses
--issues-txt instead of --issues-tests to make sure the traces do not regress.
This change would make this approach more widespread.
Reviewed By: sblackshear
Differential Revision: D4159597
fbshipit-source-id: 9c83952
Summary:
When loading results from a json file, sort them. This prints results in some
sane order for both --issues-test and --issues-txt, removing the need for
post-processing of the result.
Reviewed By: cristianoc
Differential Revision: D4167029
fbshipit-source-id: 37e9f1c
Summary:
Instead of the custom filtering done by `InferPrint --issues-tests`, use the
filtering done by `infer` and run without filtering for our e2e tests. We still
test the filtering for our build systems integration tests, and this diff
restores that behaviour for the ant test (hence the bugs removed from
ant/issues.exp).
Also add internal exceptions to most tests to get more signal out of them (eg,
knowing when we add assertion failures and the like).
Retire the old `--issues-tests` to limit the number of ways we do filtering.
Reviewed By: jeremydubreil
Differential Revision: D4131308
fbshipit-source-id: 35805cc
Summary:
This makes the tests depend on much fewer phony targets, thus reducing the need
to rerun the tests when nothing has changed.
Reviewed By: jberdine
Differential Revision: D4118457
fbshipit-source-id: 664b6e3
Summary:
Rename symbols in test files so they are not duplicated and files can be analyzed together without affecting analysis results.
Fix some compilation errors, where files could be analyzed but would fail direct compilation.
Add Makefile mimicking the same analysis parameters used for the existing tests.
Reviewed By: dulmarod
Differential Revision: D3869993
fbshipit-source-id: 6db1baf
Jeremy Dubreil
Jia Chen
Dulma Churchill
Paco Estevez Garcia
Andrzej Kotulski
Josh Berdine
Cristiano Calcagno
Jules Villard