Summary:
TOPL properties are essentially automata, which will be modeled as a set
of procedures. The code-to-analyze makes calls into these procedures,
thereby driving the automaton. In this commit, these calls do not do
anything. The point is to prepare the hook-up mechanism.
Reviewed By: jvillard
Differential Revision: D14819650
fbshipit-source-id: d95ecdb3d
Summary:
Sometimes in debug mode, the condition set is too big to print in the
log file. This diff limits the maximum number of conditions to print
as 30.
Reviewed By: mbouaziz
Differential Revision: D12836661
fbshipit-source-id: 8ddfe64a7
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
`IList.map_changed` relies on `take_append`.
The existing code was a `take_rev_append` instead.
Fixed it.
Tests are still passing, we might want to look at callsites and consider a `map_changed_unordered`.
Reviewed By: jvillard
Differential Revision: D8201187
fbshipit-source-id: 151b95c
Summary:
Append can be costly, let's do it once only.
Depends on D8185619
Reviewed By: jeremydubreil
Differential Revision: D8185634
fbshipit-source-id: 67f84a9
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:
There's actually a nice separation between IR/, base/, istd/, and the rest of
infer, so they can be made into separate jbuilder libraries so that the
separation remains. This helps make sense of the infer codebase.
Also:
- move everything biabduction-related out of backend/ and into a new
biabduction/ directory. This clarifies the current situation where backend/
contains a mix of analysis-independent code (still there now), and
biabduction-specific code (moved to biabduction/).
- move everything from base/ that is not infer-specific into istd/, e.g. IList.ml
- kill unused `FbTraceCalls`
- A couple of files needed to move around to complete the separation of base/ and IR/
Reviewed By: mbouaziz
Differential Revision: D7381842
fbshipit-source-id: cd86dea
Summary:
There's no real reason not to use `Core` lists in this module. Changed the
interface to be more `Core`-like. Changed the `*_changed` functions to use a
ref to track changes instead of passing the changed state around.
Reviewed By: mbouaziz
Differential Revision: D7123211
fbshipit-source-id: b27791a
Summary:
Just a bunch of minor changes.
- The mutable field doesn't need to be mutable: it's only mutated once in the code somewhere that doesn't even need to mutate
- Hence the type can be public
- All the `ms_get_*` functions are replaced by field accesses
- `CMethod_signature` -> `CMethodSignature` while I'm at it, although maybe that's bad since other files in clang/ follow the former convention
- `type method_signature` -> `type t`
- `pp` function instead of `to_string`, since it's used with `fprintf`. This gets rid of the only caller of `IList.to_string`.
Reviewed By: dulmarod
Differential Revision: D7123795
fbshipit-source-id: fdfae42
Summary:
`Sequence` API to walk over free variables in expressions, instead of computing lists with uniqueness constraints that make them have linear complexity for insertion.
Switch to a Set representation when we don't care about the order of elements,
otherwise to a `Hash_queue`:
https://ocaml.janestreet.com/ocaml-core/113.33/doc/core/Std/Hash_queue.mod/S.modt/
Often, we don't even need to compute the sequence of free variables, as we are
just testing membership/emptiness/...
Reviewed By: mbouaziz
Differential Revision: D7099294
fbshipit-source-id: e96f84b
Summary:
It supports flexible array member using the following heuristic:
- a memory for a class is allocated by `malloc(sizeof(C) + n * sizeof(T))` format
- the last field of the class is an array
- the static size of the last field is one, i.e., `T field_name[1]`
When allocating and initializing members of classes, it sets the size of flexible array to `n+1` if the above conditions are met.
Reviewed By: mbouaziz
Differential Revision: D7056291
fbshipit-source-id: 31c5868
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:
Change ocamlformat installation procedure to use opam instead of
pinning.
Reformat all code with v0.2, which has a few improvements.
Reviewed By: jvillard
Differential Revision: D6292057
fbshipit-source-id: 759967f
Summary:
:
Make both buck capture and compilation database handle buck command line arguments and invoke buck query the same way.
Plus allow:
- target patterns `//some/dir:` and `//some/dir/...`. However since `//some/dir:#flavor` and `//some/dir/...#flavor` are not supported, they need to be expanded before adding the infer flavor.
- target aliases (defined in `.buckconfig`)
- shortcuts `//some/dir` rewritten to `//some/dir:dir`
- relative path `some/dir:name` rewritten to `//some/dir:name`
Reviewed By: jvillard
Differential Revision: D5321087
fbshipit-source-id: 48876d4
Summary:
Install ocamlformat from github as part of `make devsetup`, and use it
for formatting OCaml (and jbuild) code.
Reviewed By: jvillard
Differential Revision: D6092464
fbshipit-source-id: 4ba0845
Summary:
This simplifies the jbuild files: no need to list these files explicitly
anymore, nor to exclude them explicitly from the main `InferModules` library
(due to their different compilation flags).
Isolate common parts into jbuild.common do `cat`-based code inclusion into
jbuild files to factorize code.
Reviewed By: jberdine
Differential Revision: D5678328
fbshipit-source-id: 6d7d925
Jeremy Dubreil
Radu Grigore
Jules Villard
Sungkeun Cho
Mehdi Bouaziz
Josh Berdine
Daiva Naudziuniene
Dulma Churchill