Summary:
The gist of this diff is a set of Pulse models for the built-ins
that have been put in Sil by the Erlang frontend:
- __erlang_make_nil, for creating an empty list like []
- __erlang_make_cons, for creating a nonempty list like [1|[]]
- __erlang_pattern_fail, which marks that no pattern matched
The models for the first two update the abstract state. The model for
the third generates a reportable error.
The diff also includes a test.
And also a few bugfixes:
- a type ErlangAny was used sometimes instead of ErlangAny*
- a load that was meant to be n=13 was instead n=*13;
changed to (*tmp=13; n=*tmp)
- the Makefile's guard for the rebar build-system test was inside the large
guard for java analyzers; of course, we don't need java to run rebar
Reviewed By: jvillard
Differential Revision: D29230161
fbshipit-source-id: c8fd6d88a
Summary:
There's been regressions in --pulse-isl. Without tests, everything is
temporary!
Note: the regressions are presumably still there, this just records the
current status of pulse.isl.
Also, no objective-C(++) at the moment. Should we add them too? (in
another diff)
Reviewed By: skcho
Differential Revision: D28256703
fbshipit-source-id: 700b2cc57
Summary:
Added a simple Erlang project to be used as a test for Rebar3
integration, in the following commits. Also, updated the copyright
linter to understand Erlang.
Reviewed By: ngorogiannis, mmarescotti
Differential Revision: D28096899
fbshipit-source-id: 94f15c277
Summary:
This diff renames and moves the opam package definition files to
`<package>.opam` in an `opam` directory at the root of the
repository. This enables opam pinning the different packages contained
in the repo. It is necessary for these files to be either at the root
of the repo or in a directory named `opam` at the root of the repo, or
else opam cannot find them.
Reviewed By: skcho
Differential Revision: D27326495
fbshipit-source-id: 4c95c6955
Summary: A little bit of sed to adjust links (see previous commit for effect).
Reviewed By: skcho
Differential Revision: D27360106
fbshipit-source-id: 2fa32f05f
Summary:
Move where the cost tests are wired into the main Makefile depending on
whether clang/Java/ObjC are supported.
This isn't used as part of `make test`, these are convenience targets to select cost tests. I often use `make show-targets | grep something | xargs make -j 4` and having non-buildable targets there (in my case objc ones) doesn't work.
Reviewed By: skcho
Differential Revision: D27052891
fbshipit-source-id: 4a4dfd75f
Summary:
This diff runs `infer reportdiff` on config impact results, ie previous and current
`config-impact-report.json`s. Ungated and added/removed callees are reported at `introduced.json`.
Reviewed By: ezgicicek
Differential Revision: D26723054
fbshipit-source-id: efabd0d5f
Summary: We forgot to add `objc_fb-gk-interaction` to Makefile which could cause its test failures to go undetected since we didn't run them on CI.
Reviewed By: skcho
Differential Revision: D26612620
fbshipit-source-id: 0b9c7edd1
Summary:
Dear Infer team,
To contribute to Infer community, I would like to integrate infer#'s language agnostic layer into Infer.
Please help to review, discuss and consider to merge this feature.
Thanks,
Xiaoyu
Pull Request resolved: https://github.com/facebook/infer/pull/1361
Reviewed By: skcho
Differential Revision: D25928458
Pulled By: jvillard
fbshipit-source-id: 7726150b8
Summary:
Now that the buck java flavour is fully deployed, the genrule-based integrations for java can be removed. We also remove the combined (clang+java) integration as this will be reimplemented using flavours in the future.
Also, remove a bunch of deprecated arguments linked to these integrations.
Reviewed By: jvillard
Differential Revision: D26104384
fbshipit-source-id: 6b0059407
Summary: This is a complex enough feature so iterating on it in a safe manner will be useful.
Reviewed By: artempyanykh
Differential Revision: D24725406
fbshipit-source-id: 81b247143
Summary:
- rename the checker "Uninitialized Variable" to "Uninitialized Value"
as this is the name of the issue type
- delete timestamp XML comment from the man pages to avoid future git
churn when updating the website
- counting is hard
Reviewed By: martintrojer
Differential Revision: D24219165
fbshipit-source-id: cf3057373
Summary:
`make new-website-version` would fail if run a second time, because it
assumes the version is brand new. Now, it will delete previous traces of
the new version, which allows one to easily update commits upgrading the
website instead of reverting the diff then running `make
new-website-version` again.
Reviewed By: martintrojer
Differential Revision: D24218463
fbshipit-source-id: 61f416677
Summary:
This can be used to push a new version of the website when publishing a
new version of infer.
Reviewed By: martintrojer
Differential Revision: D24193377
fbshipit-source-id: d2f357558
Summary:
This diff extends inferbo's domain to include closure values. The goal of this extension is to
follow missing semantics where closures are handled as values, for example, a closure is assigned to
an object field, then it is got later to call.
Due to the bottom-up nature of the analyzer, sometimes we don't know which values are written in a
field, which is the same for the other non-closure values.
Reviewed By: ezgicicek
Differential Revision: D23932186
fbshipit-source-id: 4a575d0de
Summary:
Testing procedure for java source parser
- we can run directly the parser without compiling and analysing the source file
- we add a test file
Reviewed By: ngorogiannis
Differential Revision: D23705199
fbshipit-source-id: 2103c1681
Summary:
When inspecting silent introduced issues, we found that an introduced issue is about a complexity increase of a block that is only created in the current diff. Based on the trace view, we find out that this is caused by infer mistakingly consider another block that exists in the previous diff as the same block that is newly created in the current diff.
This diff adds a test case that reproduces this case, and this will be fixed in the next diff.
facebook
Trace view: https://www.internalfb.com/intern/traceview/?id=109896337
Reviewed By: ezgicicek
Differential Revision: D23681550
fbshipit-source-id: 78341268b
Summary: Since D20891116 (224e0b7c52), java models are not installed at all if the C analyzers are not enabled. The recent move of models into Sqlite (D23191601 (1db53f43b5)) makes this a fatal error instead of a silent one.
Reviewed By: artempyanykh
Differential Revision: D23565074
fbshipit-source-id: 3816ac797
Summary:
Store model summaries in the `model_specs` database table instead of in spec files.
This table is populated when a new database is created by loading a dump of the `specs` table in the models database. This avoids the perf and reliability implications of ATTACHing the same, non-read-only models-DB by many processes.
- `BiabductionModels` is moved into `IR` so that `JsonReports` can access it.
- The binary `sqlite3` is now required on the host compiling infer.
Reviewed By: skcho
Differential Revision: D23191601
fbshipit-source-id: 1532481ee
Summary:
Before: 3 modes: (where "lenient" build has warnings not crash the
build, while "strict" build errors on warning):
- opt (default): flambda optimisations + lenient build
- dev (recommand for dev): lenient build, no flambda
- test: strict build (used in tests), no flambda
Now:
- dev (default): *strict* build, no flambda
- opt: lenient build, flambda
- dev-noerror: lenient build, no flambda (use when you want to test
infer but there are build warnings)
The goal is to give faster feedback to infer developers and reduce the
amount of times diffs are sent with build warnings. Also it's now faster
to alternate between changing infer and running unit tests since test
mode is just dev mode.
Reviewed By: ngorogiannis
Differential Revision: D23167416
fbshipit-source-id: d663b6054
Summary:
When install_name_tool fails to patch rpath (and we've seen such cases
in the wild; can happen for many reasons) we better fail the build rather
than ship the binary that will likely fail on start unless a user
happens to have gmp and sqlite dylibs installed.
Reviewed By: skcho
Differential Revision: D23187313
fbshipit-source-id: 83afd0992
Summary: New, experimental for now, integration with buck on Java using the `#infer-java-capture` flavor.
Reviewed By: artempyanykh
Differential Revision: D22187748
fbshipit-source-id: 62cdafe6b
Summary:
## Issue
There are a number of times when users building `facebook-clang-plugins` hit memory limitations, typically due to the OOM killer and when linking.
In https://github.com/facebook/facebook-clang-plugins/pull/21, I implemented support for building `facebook-clang-plugins` using both Ninja and to only use one process when linking.
## Resolution
This PR exposes the optional flags added in https://github.com/facebook/facebook-clang-plugins/pull/21 to `build-infer.sh`, such that you can build `facebook-clang-plugins` with either just `ninja` or `ninja` + only one process for linking.
As part of this, it updates the `facebook-clang-plugins` submodule.
update-submodule: facebook-clang-plugins
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
Pull Request resolved: https://github.com/facebook/infer/pull/1283
Reviewed By: dulmarod
Differential Revision: D22334307
Pulled By: jvillard
fbshipit-source-id: 97fc1c7db
Summary: This linters were not used much anymore, so we can delete them.
Reviewed By: ngorogiannis
Differential Revision: D22233895
fbshipit-source-id: f31180a05
Summary: There is now a compilation check for UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK so this check is less useful. Also the check REGISTERED_OBSERVER_BEING_DEALLOCATED is useful only in an old version of iOS.
Reviewed By: ngorogiannis
Differential Revision: D22231851
fbshipit-source-id: 72151fef5
Summary:
A space in user's path will lead to a make failure on line 899 of
Makefile. Let's espace the path to avoid that.
Reviewed By: jvillard
Differential Revision: D22044934
fbshipit-source-id: 5a949be1d
Summary:
This diff adds a prototype of a new checker that collects config checkings between markers.
Basically, what the checker is doing is a taint analysis.
* Taint source: function calls of "marker start"
* Taint sink: function calls of config checking
* Taint remove: function calls of "marker end"
By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending.
I am separating the diff into three steps:
(1/3) Add basic abstract semantics
(2/3) Add trace information
(3/3) Add reporting with test examples
Reviewed By: jvillard
Differential Revision: D21998170
fbshipit-source-id: e7759f62f
Summary:
Turns out it was useful, so it is now reborn in OCaml.
Fixes https://github.com/facebook/infer/issues/1262.
Reviewed By: skcho
Differential Revision: D22016185
fbshipit-source-id: 31ccb7540
Summary:
Hopefully solve issues with people having versions of sqlite that make
infer crash.
Fix#1081.
Reviewed By: skcho
Differential Revision: D21998757
fbshipit-source-id: 4baabc1c3
Summary:
This is mostly a partial revert of D19022905 and D19272627 for only the
part of it concerned with "install-with-libs".
Fixes#1260.
Reviewed By: skcho
Differential Revision: D21998484
fbshipit-source-id: ed884e772
Summary:
Write documentation for all documented issue types and all user-facing
checkers in the "next" version of the documentation. Next diff shows the
new website.
Reviewed By: dulmarod
Differential Revision: D21934370
fbshipit-source-id: 53315d2b4
Summary: We were missing `performance-exclusive` and `fb-performance` tests in the list of cost analysis targets.
Reviewed By: jvillard
Differential Revision: D21837972
fbshipit-source-id: 550d27918
Summary:
infer/src/deadcode/dune.in is not an OCaml-syntax dune file, so
exclude it from the list computed for use by the auto-formatter.
Reviewed By: jvillard
Differential Revision: D21583047
fbshipit-source-id: 13a99a89b
Summary:
Start with tests about dynamic dispatch to test the upcoming
pre-analysis.
Reviewed By: ezgicicek
Differential Revision: D21594496
fbshipit-source-id: 1771ea968
Summary:
Fix `make doc-publish` and make it publish the documentation to
website/static/{man,doc}/next/.
Reviewed By: ngorogiannis
Differential Revision: D21552291
fbshipit-source-id: fb6d07cfc
Radu Grigore
Sungkeun Cho
Jules Villard
Artem Pianykh
Josh Berdine
Ezgi Çiçek
Martin Trojer
Xiaoyu Liu
Nikos Gorogiannis
Mitya Lyubarskiy
David Pichardie
Qianyi Shu
Andrew V. Jones
Dulma Churchill