Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.
Reviewed By: jvillard
Differential Revision: D14477671
fbshipit-source-id: c38a8ef37
Summary:
Add an option to specify some classes that we really want to warn about
with the liveness checker, even when they appear used because of the
implicit destructor call inserted by the compiler.
Reviewed By: mbouaziz
Differential Revision: D13991129
fbshipit-source-id: 7fafdba84
Summary:
Add the `--source-files-cfg` option to emit CFGs as .dot files just as if one
had run with `--debug` to begin with. The usual `--source-files-filter`
applies. For example:
```
$ cd examples
$ infer -- clang -c hello.c
$ infer --continue -- javac Hello.java
$ infer --continue -- make -C c_hello
$ infer explore --source-files --source-files-cfg --source-files-filter ".*\.c$"
hello.c
c_hello/example.c
CFGs written in /home/jul/infer.fb/examples/infer-out/captured/*/icfg.dot
```
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D13973062
fbshipit-source-id: 3077e8b91
Summary:
Change join/widen policies to more interesting ones and play around to
find a good tradeoff.
Reviewed By: mbouaziz
Differential Revision: D13432492
fbshipit-source-id: 2c3e498dd
Summary: Experimental feature: Use memcached for summaries as a look-aside cache during analysis.
Reviewed By: jvillard
Differential Revision: D12939311
fbshipit-source-id: 9f78994e2
Summary: Reports will now be issued for the class loads of the methods specified by the option `--class-loads-roots`.
Reviewed By: jvillard
Differential Revision: D10466492
fbshipit-source-id: 91456d723
Summary: First version of an analyzer collecting classes transitively touched.
Reviewed By: mbouaziz
Differential Revision: D10448025
fbshipit-source-id: 0ddfefd46
Summary:
New analysis in foetal form to detect invalid use of C++ objects after their
lifetime has ended. For now it has:
- A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended)
- The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid.
- A simple transfer function reads and updates the stack and heap in a rudimentary way for now
- C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations
- Also, the domain has a really crappy join and widening for now (see comments in the code)
With this we already pass most of the "use after delete" tests from the
Ownership checker. The ones we don't pass are only because we are missing
models.
Reviewed By: mbouaziz
Differential Revision: D10383249
fbshipit-source-id: f414664cb
Summary:
Sometimes the default timeout of 10s is not enough(!). Make it
configurable while we work on not hitting it anyway.
Reviewed By: da319
Differential Revision: D10083772
fbshipit-source-id: ab949039f
Summary:
Keep `--analyzer` around for now for integrations that depend on it.
Also deprecate the `--infer-blacklist-path-regex`,
`--checkers-blacklist-path-regex`, etc. in favour of
`--report-blacklist-path-regex` which more accurately represents what these do
as of now.
Rely on the current subcommand instead of the analyzer where needed, as most of
the code already does.
Reviewed By: jeremydubreil
Differential Revision: D9942809
fbshipit-source-id: 9380e6036
Summary: Use the value of other options instead since we're trying to get rid of it. This should be equivalent.
Reviewed By: jeremydubreil
Differential Revision: D9943274
fbshipit-source-id: 055e1bdd2
Summary:
The method matcher is now used sufficiently it warrants refactoring out into its own module.
Also, kill dev-android-strict-mode and leave starvation-strict-mode as the stronger option.
Reviewed By: jeremydubreil
Differential Revision: D9990753
fbshipit-source-id: 626a70a19
Summary:
This adds an option `--trace-events` that generates a Chrome trace event[1] to
quickly visualise the performance of infer.
Reviewed By: mbouaziz
Differential Revision: D9831599
fbshipit-source-id: 96a33c627
Summary:
For some unexplained reason, some of the functions registered in the Epilogues would sometimes be executed several times. I could not figure out why.
This diff fixes that, but also has more explainable benefits:
- Do not run epilogues registered in the parent in the children. Previously it
would do so, but probably only if the children registered some epilogue given
that `at_exit` must be called again once on the child (but the value of the ref
in `Pervasives` would not have been reset).
- Unified behaviour for early and late epilogues given that we now handle both of these directly
We already have all the control needed to run epilogues when needed: we know
when infer exits, and we know when children processes exit.
Reviewed By: mbouaziz
Differential Revision: D9752046
fbshipit-source-id: 13af40081
Summary:
Turn off by default until mature enough.
Also rename the dev-strict-mode test dir to highlight the dev part.
Reviewed By: mbouaziz
Differential Revision: D9775571
fbshipit-source-id: c3a41bbdf
Summary:
First step in writing an analyzer that is meant to run only on Android core library implementation.
This will, when finished, compute the library entrypoints that may lead to a strict mode violation.
The normal analyzer will use those to statically flag strict mode violations in app code.
Strict Mode is an Android debug mode, where doing certain things (like disk read/write or network activity) on the UI thread will raise an exception. We want to statically catch these, as well as indirect versions (the UI thread takes a lock and another thread holding that lock calls a method that would be a strict mode violation).
Reviewed By: mbouaziz
Differential Revision: D9634407
fbshipit-source-id: c30bcedb3
Nikos Gorogiannis
Radu Grigore
Jules Villard
Jeremy Dubreil
David Lively
Nikos Gorogiannis
Sungkeun Cho
Ezgi Çiçek
Dino Distefano
Mehdi Bouaziz
Julian Sutherland
Martin Trojer
Martino Luca