Summary: This could generate enormous amounts of logs on medium-sized projects (eg rocksdb) when running with `--stats`. Review other debug levels in inferbo as well.
Reviewed By: mbouaziz
Differential Revision: D5364139
fbshipit-source-id: 5c8d206
Summary:
In C++ it may happen that a procedure return 'variable' is an access
path that cannot be translated to Hil. For now just skip these instead
of crashing.
Reviewed By: mbouaziz
Differential Revision: D5356134
fbshipit-source-id: 977dfba
Summary:
They are expected to occur in C++ code, so don't fail on them. For now
just skip them, although a better treatment of dynamic dispatch may be
needed later.
Reviewed By: da319, mbouaziz
Differential Revision: D5292462
fbshipit-source-id: 4285514
Summary:
Indexing into a string literal expression would generate a fresh
variable on every application of a transformer. This violated
finiteness of the domain, and caused divergence.
Reviewed By: da319
Differential Revision: D5342951
fbshipit-source-id: e95e84e
Summary: It was passing the argument multiple times rather than once with all the accepted values
Reviewed By: jvillard
Differential Revision: D5338509
fbshipit-source-id: 22b86a5
Summary: This is useful when we only want to examine the html for some but not all source files.
Reviewed By: jvillard
Differential Revision: D5334786
fbshipit-source-id: 774c23c
Summary:
It instantiates fields of structures when a pointer to which is given
as a function parameter, e.g., `foo(&s);`.
Reviewed By: mbouaziz, jvillard
Differential Revision: D5337645
fbshipit-source-id: c06da29
Summary: Rename historical option to its new form, since the old form was no longer accepted by infer.
Reviewed By: martinoluca
Differential Revision: D5329033
fbshipit-source-id: 4fa9402
Summary:
We keep track of both `beginPtr` and `endPtr` but the modelling was mostly
about `beginPtr` as some sort of approximation I guess. This shouldn't change
much but will be useful later when doing more iterator stuff.
Reviewed By: mbouaziz
Differential Revision: D5255772
fbshipit-source-id: 0f6e3e8
Summary:
This will be needed to re-use the functions now in Driver.ml in other contexts
without always adding to infer.ml. For instance, this is used in a later diff
to do a diff-analysis orchestrator that needs to run the capture and analysis
several times.
Reviewed By: jberdine
Differential Revision: D5319862
fbshipit-source-id: caf9551
Summary: Needed in a later diff to be able to compute the set of changed files *during* an infer execution.
Reviewed By: jberdine
Differential Revision: D5319667
fbshipit-source-id: 226ec91
Summary: This seems to move in the right direction. Also, `const operator[]` did not do an `access_at`, which I fixed.
Reviewed By: mbouaziz
Differential Revision: D5320427
fbshipit-source-id: c31c5ea
Summary: Unknown library returns the unknown pointer as well as the top interval.
Reviewed By: mbouaziz, jvillard
Differential Revision: D5282669
fbshipit-source-id: 34c7e18
Summary:
Thanks to the logging introduced in D5293334 (or because of, depending on your liking of spam), I noticed that there lots of errors being logged of the form
Couldn't read multilink file '/home/jul/infer/infer/tests/codetoanalyze/cpp/errors/infer-out/attributes/d0/multilink.txt': /home/jul/infer/infer/tests/codetoanalyze/cpp/errors/infer-out/attributes/d0/multilink.txt: No such file or directory
I don't think it makes sense to care about multilink files except when `--merge` is specified.
Also introduced a .mli and self-documented a function.
Reviewed By: akotulski
Differential Revision: D5310129
fbshipit-source-id: c3a6276
Summary:
Once the fixed/preexisting/introduced sets have been computed, they endure
further filtering which may decide that more of them are equal. These bugs just
get dropped on the floor. Put these into preexisting as well instead, at least
in the case of the "skip_duplicated_types_on_filenames" filter.
Reviewed By: martinoluca
Differential Revision: D5274248
fbshipit-source-id: 99b3f3d
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:
:
There are throw wrapper functions like `std::__throw_bad_alloc()` defined in both libstdc++ (https://github.com/gcc-mirror/gcc/blob/master/libstdc%2B%2B-v3/include/bits/functexcept.h) and libc++ (e.g. 907c1196a7/include/new (L145)). Folly actually exports some of them as well (diffusion/FBS/browse/master/fbcode/folly/portability/BitsFunctexcept.h). The function body of those wrappers merely throws the corresponding exception. My understanding is that the primary purpose of the wrappers is to throw the exception if everything goes well and to fall back to something reasonable when exception is disabled (e.g. when `-fno-exceptions` is passed to the compiler).
The problem is that infer doesn't really understand what those functions do, and I've seen some false positives get reported as a result of it. So to remove those FPs we need to either model them or handle them specially. Modeling those wrappers by either whitelisting them or overriding the include files turns out to be difficult, as those wrappers are only declared but not defined in the STL headers. Their implementations are not available to Infer so whitelisting them does nothing, and if I provide custom implementations in the headers then normal compilation process will be disrupted because the linker would complain about duplicated implementation.
What I did here is to replace functions whose name matches one of the throw wrapper's name with a `BuiltinDecls.exit`. I have to admit that this is a bit hacky: initially I was trying to do something more general: replacing functions with `noreturn` attribute with `BuitinDecls.exit`. That did not work because, CMIIW, the current frontend only exports function attributes for functions with actual bodies, not declaration-only functions. I'd love to be informed if there are better ways to handle those wrappers.
Reviewed By: jeremydubreil
Differential Revision: D5266030
fbshipit-source-id: 4580227
Summary:
:
Do not store dummy `_` into the stack.
This makes debugging a lot easier
Reviewed By: skcho
Differential Revision: D5275941
fbshipit-source-id: ce329a5
Jules Villard
Jia Chen
Josh Berdine
Kihong Heo
Martino Luca
Jeremy Dubreil
Daiva Naudziuniene
Alexander Slesarev
Radu Grigore
Sungkeun Cho
Andrzej Kotulski
Dino Distefano
Dulma Churchill
Sam Blackshear
Mehdi Bouaziz