Summary: Previously there was no way of getting that list from the manual.
Reviewed By: jeremydubreil
Differential Revision: D15158598
fbshipit-source-id: 1705ed59d
Summary:
A more dynamic scheduling scheme will potentially run into the situation where no new work packets can be scheduled, but more work will be possible to schedule in the future, perhaps when some dependent work packet finishes being analysed.
The current implementation prevents that, as it expects that if a worker goes idle, it stays idle.
The changes here address this in two parts:
- the `select` call is always given a finite timeout. If given an infinite timeout, we will not be able to poll the task generator for more work, where none were previously possible.
- when the `select` call times out without updates, check if there is an idle child, and if so if the task generator has more work right now.
See also ProcessPool.mli for comments.
Reviewed By: mbouaziz
Differential Revision: D15197749
fbshipit-source-id: babe5da8e
Summary:
Before moving to any kind of non-trivial scheduling, we need to change the Tasks interface.
In particular, it's too restrictive to expect that the tasks to be scheduled are provided as a list before starting execution. For example, dynamic scheduling does not fit the bill here. Also, the list expectation means all scheduling work has to be done up front.
The solution here is to move to a `Sequence`-like interface with one difference:
- The function returning the next task expects a task option argument. That argument is the task that was just finished (if any) by the worker expecting new work. This will be useful for things like task dependencies (for instance, a procedure has been analysed, and can be marked so).
Reviewed By: mbouaziz
Differential Revision: D15181613
fbshipit-source-id: 21f3ba825
Summary:
Adds option `--summary-stats` to `infer report`.
The formatting is not perfect yet but it gives what I want.
Reviewed By: ngorogiannis
Differential Revision: D15064162
fbshipit-source-id: 56c4b4929
Summary: There was a missing case for singleton monomials of degree > 1.
Reviewed By: mbouaziz
Differential Revision: D15098810
fbshipit-source-id: e6d17d899
Summary:
Boolean Xor expressions are treated directly by the solver, so the 'no
new subexps' invariant for congruence closure is not needed.
Reviewed By: mbouaziz
Differential Revision: D15098817
fbshipit-source-id: d118c5881
Summary: Shifting by too many bits is undefined, so do not normalize them.
Reviewed By: mbouaziz
Differential Revision: D15098812
fbshipit-source-id: 96f4606d7
Summary:
When constructing division expressions from rational coefficients of
polynomials, the constant numerator and denominator should be clamped
to the number of bits in the result type.
Reviewed By: mbouaziz
Differential Revision: D15098825
fbshipit-source-id: fa448c39a
Summary:
Some constants are used during Exp normalization, to encode
subtraction using addition, units of addition and multiplication,
etc. Previously these were unconditionally integers, but need to be
floats for float arithmetic.
Reviewed By: mbouaziz
Differential Revision: D15098815
fbshipit-source-id: 13d1be142
Summary:
The frontend would implicitly assume there was (at least) one argument
to calls to operator new. If code declares operator new with the wrong
type, this can lead to crashing trying to access a missing arg.
Reviewed By: mbouaziz
Differential Revision: D15098820
fbshipit-source-id: 539281a83
Summary: These relaxations are needed for some of the llvm test suite.
Reviewed By: mbouaziz
Differential Revision: D15098813
fbshipit-source-id: 702d3ffd9
Summary:
Some globals have initializers which refer to the global
itself (e.g. for program counter relative offsets). Memoizing
translation of globals gives enough machinery to detect and handle
this situation.
Reviewed By: mbouaziz
Differential Revision: D15098819
fbshipit-source-id: ecc9dce92
Summary:
In some cases there were extra metadata operands (such as alignment of
an alloc) which would cause the debug locations to not be recorded.
Reviewed By: mbouaziz
Differential Revision: D15098816
fbshipit-source-id: a7e83f590
Summary:
This reverts commit e4f7a0dc8d439561a0be7e8b33ad924195a6c441.
No longer needed due to ocamlformat fix.
Reviewed By: mbouaziz
Differential Revision: D15098826
fbshipit-source-id: 2a4dc0f55
Summary: No reason to use custom function name and not implement `Hashable`.
Reviewed By: mbouaziz
Differential Revision: D15097603
fbshipit-source-id: 7303fc15e
Summary: Remove from inferbo summary locations that are unreachable from callers
Reviewed By: ezgicicek
Differential Revision: D15064518
fbshipit-source-id: 734e79b4a
Summary: Using `Fields.to_list` also makes sure we don't forget fields.
Reviewed By: ezgicicek
Differential Revision: D15062353
fbshipit-source-id: aaac9be99
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: The name was misleading, the function only forget locs for relations.
Reviewed By: ezgicicek
Differential Revision: D15045933
fbshipit-source-id: 7f41a55e7
Summary:
- `--source-files` was missing.
- The three modes are actually independent, make it clearer and group options by mode.
- Fail if `--procedures` and `--source-files` are used together.
Reviewed By: jeremydubreil
Differential Revision: D15049822
fbshipit-source-id: cc515cb56
Summary:
Replace `$(u,...)` with `$(i,...)` since `$(u,...)` doesn't exist.
Cmdliner was emitting a warning at runtime:
cmdliner error: Unknown cmdliner markup $(u,...) in "Specify classes where the destructor should be ignored when computing liveness. In other words, assignement to variables of these types (or common wrappers around these types such as $(u,unique_ptr<type>)) will count as dead stores when the variables are not read explicitly by the program. (default: $(i,[]))"
Reviewed By: mbouaziz
Differential Revision: D15045004
fbshipit-source-id: e03ece4f7
Summary:
A long-standing easter egg from infer error messages is the "object
`null` could be null and is dereferenced at line ...". I tried to fix
this but the part that generates the first "null" in the message and the
part that generates the second one are very far apart and it's hard to
see how to make the second part aware of the first in a clean way.
Instead, hack around it by detecting if the string representing the
value is literally `null` and in that case chop `could be null ` from
the error messages...
Reviewed By: jeremydubreil
Differential Revision: D14972324
fbshipit-source-id: ccc48ce6b
Nikos Gorogiannis
Jules Villard
Dino Distefano
Jeremy Dubreil
Ezgi Çiçek
Mehdi Bouaziz
Josh Berdine
David Lively
Radu Grigore