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:
Error'ing when getting several subcommands on the command line only makes sense
when the user typed these options herself. This was causing a bug in the Gradle
integration, and possibly others (see GitHub issue).
Fixes#668
Reviewed By: jeremydubreil
Differential Revision: D5381850
fbshipit-source-id: f332377
Summary:
Fixes#683
Disclaimer: I don't know what XML namespaces/namespace prefixes are, but this seems to do the trick.
Reviewed By: mbouaziz
Differential Revision: D5381480
fbshipit-source-id: 3da16e7
Summary: This will allow to replace type vars into concrete types in expressions.
Reviewed By: jvillard, mbouaziz
Differential Revision: D5209276
fbshipit-source-id: c1650f8
Summary:
The thread safety domain manipulates access paths that are a variable
followed by a sequence of field or index accesses. Some expressions
from C++ code do not fit that form, such as cases where subtraction of
an offset from a pointer is used to obtain another pointer, whose
fields are then accessed. Previously the analyzer would crash on such
expressions. This diff partially treats them by introducing dummy
variables.
Reviewed By: da319
Differential Revision: D5343567
fbshipit-source-id: f73b520
Summary:
:
Get rid of model location in reports.
The goal is to avoid changing `issues.exp` whenever a model is updated.
Reviewed By: jvillard
Differential Revision: D5356608
fbshipit-source-id: 88ecaba
Summary: This could generate enormous amounts of logs on medium-sized projects (eg rocksdb) when running with `--stats`. Review other debug levels in inferbo as well.
Reviewed By: mbouaziz
Differential Revision: D5364139
fbshipit-source-id: 5c8d206
Summary:
In C++ it may happen that a procedure return 'variable' is an access
path that cannot be translated to Hil. For now just skip these instead
of crashing.
Reviewed By: mbouaziz
Differential Revision: D5356134
fbshipit-source-id: 977dfba
Summary:
They are expected to occur in C++ code, so don't fail on them. For now
just skip them, although a better treatment of dynamic dispatch may be
needed later.
Reviewed By: da319, mbouaziz
Differential Revision: D5292462
fbshipit-source-id: 4285514
Summary:
Indexing into a string literal expression would generate a fresh
variable on every application of a transformer. This violated
finiteness of the domain, and caused divergence.
Reviewed By: da319
Differential Revision: D5342951
fbshipit-source-id: e95e84e
Summary: This is useful when we only want to examine the html for some but not all source files.
Reviewed By: jvillard
Differential Revision: D5334786
fbshipit-source-id: 774c23c
Summary:
It instantiates fields of structures when a pointer to which is given
as a function parameter, e.g., `foo(&s);`.
Reviewed By: mbouaziz, jvillard
Differential Revision: D5337645
fbshipit-source-id: c06da29
Summary: Rename historical option to its new form, since the old form was no longer accepted by infer.
Reviewed By: martinoluca
Differential Revision: D5329033
fbshipit-source-id: 4fa9402
Summary:
We keep track of both `beginPtr` and `endPtr` but the modelling was mostly
about `beginPtr` as some sort of approximation I guess. This shouldn't change
much but will be useful later when doing more iterator stuff.
Reviewed By: mbouaziz
Differential Revision: D5255772
fbshipit-source-id: 0f6e3e8
Summary:
This will be needed to re-use the functions now in Driver.ml in other contexts
without always adding to infer.ml. For instance, this is used in a later diff
to do a diff-analysis orchestrator that needs to run the capture and analysis
several times.
Reviewed By: jberdine
Differential Revision: D5319862
fbshipit-source-id: caf9551
Summary: Needed in a later diff to be able to compute the set of changed files *during* an infer execution.
Reviewed By: jberdine
Differential Revision: D5319667
fbshipit-source-id: 226ec91
Summary: Unknown library returns the unknown pointer as well as the top interval.
Reviewed By: mbouaziz, jvillard
Differential Revision: D5282669
fbshipit-source-id: 34c7e18
Summary:
Thanks to the logging introduced in D5293334 (or because of, depending on your liking of spam), I noticed that there lots of errors being logged of the form
Couldn't read multilink file '/home/jul/infer/infer/tests/codetoanalyze/cpp/errors/infer-out/attributes/d0/multilink.txt': /home/jul/infer/infer/tests/codetoanalyze/cpp/errors/infer-out/attributes/d0/multilink.txt: No such file or directory
I don't think it makes sense to care about multilink files except when `--merge` is specified.
Also introduced a .mli and self-documented a function.
Reviewed By: akotulski
Differential Revision: D5310129
fbshipit-source-id: c3a6276
Summary:
Once the fixed/preexisting/introduced sets have been computed, they endure
further filtering which may decide that more of them are equal. These bugs just
get dropped on the floor. Put these into preexisting as well instead, at least
in the case of the "skip_duplicated_types_on_filenames" filter.
Reviewed By: martinoluca
Differential Revision: D5274248
fbshipit-source-id: 99b3f3d
Summary:
This diff tries to achieve the followings: if we have the following C++ codes:
```
bool foo(int x, int y) {
return &x == &y;
}
```
We want the C++ frontend to emit Sil as if the input is written as
```
bool foo(int x, int y) {
if (&x == &y) return 1; else return 0;
}
```
This matches the behavior of our Java frontend.
The reason why we prefer an explicit branch is that it will force the backend to eagerly produce two different specs for `foo`. Without the explicit branch, for the above example the backend would produce one spec with `return = (&x == &y)` as the post condition, which is not ideal because (1) we don't want local variables to escape to the function summary, and (2) with the knowledge that no two local variables may alias each other, the backend could actually determines that `&x == &y` is always false, emitting a more precise postcondition `return = 0`. This is not possible if we do not eagerly resolve the comparison expression.
Reviewed By: akotulski
Differential Revision: D5260745
fbshipit-source-id: 6bbbf99
Summary:
:
Do not store dummy `_` into the stack.
This makes debugging a lot easier
Reviewed By: skcho
Differential Revision: D5275941
fbshipit-source-id: ce329a5
Summary:
I changed the link, so that now it works.
Closes https://github.com/facebook/infer/pull/666
Differential Revision: D5256662
Pulled By: dulmarod
fbshipit-source-id: 5ae622d
Summary: This change introduces the a new argument that lets you restrict the results of a differential report to only certain files.
Reviewed By: mbouaziz
Differential Revision: D5236626
fbshipit-source-id: 52711e9
Summary: Looks much less confusing when C++ templates with `<stuff>` are involved.
Reviewed By: mbouaziz
Differential Revision: D5255551
fbshipit-source-id: f4a93e6
Summary:
After D5245416 I was taking a closer look and decided it's best to get rid of the `Interprocedural` module altogether.
Since jeremydubreil's refactoring to pass the summaries around everywhere, this module doesn't do much (it used to make sure the summary actually got stored to disk).
Client code is shorter and simpler without this module.
Reviewed By: mbouaziz
Differential Revision: D5255400
fbshipit-source-id: acd1c00
Summary:
Only one instance will win in the end so it's not useful to double register.
Log when that happens. Currently it happens in the Java tests on
`InferBuiltins` but I don't understand why so I left it alone.
Reviewed By: jberdine
Differential Revision: D5217928
fbshipit-source-id: dc7ccca
Summary:
This avoids race conditions when two processes or more try to lock a file for
writing. It could be that the process losing the race writes less than the
winner, then we get rubbish at the end of the file. Calling `ftruncate(2)` inside the critical section makes sure the
contents of the file are erased first. The harmful race was observed in
xcodebuild sometimes, as it can call infer on the same file several times in
parallel (!).
Reviewed By: jberdine
Differential Revision: D5209177
fbshipit-source-id: 744169c
Summary: I tested on Fresco and this reduced the number of calls to Prover.check_disequal by 30%.
Reviewed By: cristianoc
Differential Revision: D5237774
fbshipit-source-id: 377545e
Summary: The docs for this said that it stores the summary to disk, which is no longer true. `compute_summary` is more descriptive of what it actually does now.
Reviewed By: jberdine
Differential Revision: D5245416
fbshipit-source-id: f5138cd
Summary: We had a model for `Pools.SimplePool`, but were missing models for `Pools.Pool`. Since `SimplePool` and `SynchronizedPool` both extend `Pool`, modeling it should cover all of the cases.
Reviewed By: ngorogiannis
Differential Revision: D5236280
fbshipit-source-id: 9bbdb25
Summary:
When dealing with differential's comparisons, SourceFiles in reports may not exist anymore because of changes between revisions.
Disable user visible warnings if desired, through the labeled argument `~warn_on_error`
Reviewed By: jvillard
Differential Revision: D5217097
fbshipit-source-id: 7a1542b
Summary:
The ThreadSafety analysis currently reports on methods only if some
class in the file defining the method is annotated ThreadSafe, or
if it is called by some other such method call. Conflating files and
classes is a bit of a Javaism that seems to be unnecessary.
Reviewed By: sblackshear
Differential Revision: D5182319
fbshipit-source-id: aa77754
Summary: This makes it possible to see which tainted parameter can flow to a sink, which is quite useful.
Reviewed By: jeremydubreil
Differential Revision: D5213297
fbshipit-source-id: 1371b5a
Josh Berdine
Mehdi Bouaziz
Dulma Churchill
Jules Villard
Jia Chen
Andrzej Kotulski
Kihong Heo
Jeremy Dubreil
Daiva Naudziuniene
Radu Grigore
Sungkeun Cho
Dino Distefano
Sam Blackshear
Kyriakos Nikolaos Gkorogiannis
Marco Concetto Rudilosso
Martino Luca