Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each Mem domain value includes one relational value containing relations among symbols. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three symbols, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default. Use the `--bo-relational-domain {oct, poly}` option for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: jvillard
Differential Revision: D8874102
fbshipit-source-id: 08e5883cb
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each `Mem` domain value includes one relational value containing relations among *symbols*. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three *symbols*, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default, so this diff should not make any differences in CI.
Use `--bo-relational-domain {oct, poly}` for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: mbouaziz, jvillard
Differential Revision: D8478542
fbshipit-source-id: 510ff53
Summary:
Users missing the development package for libsqlite3 would see only a failure to install "sqlite3". Adding conf-sqlite3 to the dependencies does not improve things that much but there is a bit more information in the console:
```
[ERROR] The compilation of conf-sqlite3 failed at "pkg-config sqlite3".
[ERROR] The compilation of sqlite3 failed at "jbuilder build -p sqlite3 -j 4".
#=== ERROR while installing conf-sqlite3.1 ====================================#
# opam-version 1.2.2
# os linux
# command pkg-config sqlite3
# path /home/jul/.opam/infer-4.06.1+flambda/build/conf-sqlite3.1
# compiler 4.06.1+flambda
# exit-code 1
# env-file /home/jul/.opam/infer-4.06.1+flambda/build/conf-sqlite3.1/conf-sqlite3-7504-7afd23.env
# stdout-file /home/jul/.opam/infer-4.06.1+flambda/build/conf-sqlite3.1/conf-sqlite3-7504-7afd23.out
# stderr-file /home/jul/.opam/infer-4.06.1+flambda/build/conf-sqlite3.1/conf-sqlite3-7504-7afd23.err
#=== ERROR while installing sqlite3.4.3.2 =====================================#
# opam-version 1.2.2
# os linux
# command jbuilder build -p sqlite3 -j 4
# path /home/jul/.opam/infer-4.06.1+flambda/build/sqlite3.4.3.2
# compiler 4.06.1+flambda
# exit-code 1
# env-file /home/jul/.opam/infer-4.06.1+flambda/build/sqlite3.4.3.2/sqlite3-7504-d2c37b.env
# stdout-file /home/jul/.opam/infer-4.06.1+flambda/build/sqlite3.4.3.2/sqlite3-7504-d2c37b.out
# stderr-file /home/jul/.opam/infer-4.06.1+flambda/build/sqlite3.4.3.2/sqlite3-7504-d2c37b.err
### stderr ###
# -> stdout:
# [...]
# | ast_impl_magic_number: Caml1999M022
# | ast_intf_magic_number: Caml1999N022
# | cmxs_magic_number: Caml1999D022
# | cmt_magic_number: Caml1999T022
# -> stderr:
# Fatal error: exception End_of_file
# Raised at file "src/import0.ml" (inlined), line 351, characters 22-32
# Called from file "src/configurator.ml", line 511, characters 13-22
# Called from file "src/config/discover.ml", line 42, characters 2-1023
Exception:
Reqs_error
(Process_error
("opam install -y ANSITerminal.0.8 atd.1.12.0 atdgen.1.12.0 base.v0.11.0 base64.2.2.0 bin_prot.v0.11.0 biniou.1.2.0 camlp4.4.06+1 camlzip.1.07 cmdliner.1.0.2 conf-aclocal.1.0.0 conf-autoconf.0.1 conf-m4.1 conf-pkg-config.1.0 conf-sqlite3.1 conf-which.1 conf-zlib.1 configurator.v0.11.0 core.v0.11.0 "... (* string length 1469; truncated *),
Unix.WEXITED 4)).
```
Also fix some issues with `build-infer.sh`:
- fix a problem where `SCRIPT_PATH` should be `SCRIPT_DIR`
- add `set -u` and `set -o pipefail` to make sure we don't miss errors in the future
- add quotes everywhere
- make number of `JOBS` user-configurable instead of hardcoding `$NCPU`
Reviewed By: mbouaziz
Differential Revision: D8201849
fbshipit-source-id: 19b7c77
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.
Reviewed By: jvillard
Differential Revision: D7663537
fbshipit-source-id: 3e90970
Summary:
Upgrade ocamlformat to 0.3, and (necessarily) base to v0.10.0.
- Fix accumulated mis-formatting
- Update opam.lock to unbreak clean build
- Update to base v0.10.0
- Update opam.lock for base
- Update offline opam repo
- Everyone should already have removed their ocamlformat pin
- ocamlformat 0.3 supports output to stdout natively
- bump version of ocamlformat
Reviewed By: jeremydubreil
Differential Revision: D6636741
fbshipit-source-id: 41a56a8
Summary:
Deduping issues when generating a single report and then diffing the
reports can lead to introduced issues being considered duplicates of
existing issues.
Reviewed By: sblackshear
Differential Revision: D6414673
fbshipit-source-id: bba81fd
Summary:
No need for our own patched version now that it's available in opam.
You should `opam pin remove --no-action javalib && ./build-infer.sh` to get rid of the previous version.
Reviewed By: mbouaziz
Differential Revision: D6063730
fbshipit-source-id: 8efd598
Summary:
This allows us to get rid of code that copied source files individually. I
didn't migrate the various flags that could be included as it doesn't look like
that's possible yet (they depend on the context and on some configuration
options).
Reviewed By: jberdine
Differential Revision: D6051825
fbshipit-source-id: c28dd37
Summary:
Use a monotonic time source instead.
Also, sleep between retries in the Serialization code.
Reviewed By: jberdine
Differential Revision: D5941697
fbshipit-source-id: 05efbe1
Summary:
Use an SQLite database to store proc attributes, instead of files on disk.
Wrap SQLite operations in two layers:
1. `SqliteUtils` provides helper functions to make sure DB operations succeed
2. `KeyValue` provides a functor to expose a simple and type-safe key/value store backed by the SQLite DB.
Reviewed By: jberdine
Differential Revision: D5640053
fbshipit-source-id: 31050e5
Summary: `make opam.lock` shows that we can get rid of some more packages (perhaps leftovers from reason?).
Reviewed By: jberdine
Differential Revision: D5573505
fbshipit-source-id: 8b41152
Summary:
Conversion and reformat of infer source using ocamlformat
auto-formatting tool.
Current status:
- Because Reason does not handle docstrings, the output of the
conversion is not 'Warning 50'-clean, meaning that there are
docstrings with ambiguous placement. I'll need to manually fix
them just before landing.
Reviewed By: jvillard
Differential Revision: D5225546
fbshipit-source-id: 3bd2786
Summary:
Glorious, glorious man pages.
This changes a bunch of things that were hard to break up from the diff, so the
resulting diff is big.
Use `Cmdliner.Manpage` to format man pages (and also format a bit ourselves
since it is so stubborn).
As a bonus, introduce the following subcommands:
```
infer run ... # same as default mode with -- before
infer capture ... # -a capture
infer compile ... # -a compile
infer analyze ... # InferAnalyze
infer report ... # InferPrint
infer diff ... # this one is not new
infer clang ... # InferClang, not that you should use it
```
The man pages can still be improved a lot. Notable missing sections:
`ENVIRONMENT`, stuff about .inferconfig, some example usage, `DESCRIPTION`, ...
Reviewed By: jberdine
Differential Revision: D4921083
fbshipit-source-id: 9602230
Summary: This makes the build less likely to break because of package upgrades in opam.
Reviewed By: mbouaziz
Differential Revision: D4937908
fbshipit-source-id: 5ce9ec7
Sungkeun Cho
Jules Villard
Josh Berdine
Martino Luca