Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.
```
Potential deadlock.
Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```
Reviewed By: mbouaziz
Differential Revision: D8379328
fbshipit-source-id: bc33983
Summary: Deadlocks can be very noisy, so dedup reports on same line by showing only the one with the shortest trace and a count of the suppressed ones.
Reviewed By: mbouaziz
Differential Revision: D8351148
fbshipit-source-id: 8913db2
Summary: We were missing reads of `a` if it was used in void cast, i.e. `(void) a;` This caused dead store false positives: we were not using `exp` that was the result of translating `a`. This diff creates a call to built-in skip function with `exp` as its argument, which causes the analyses to see reads of `exp`.
Reviewed By: mbouaziz
Differential Revision: D8332092
fbshipit-source-id: f3b0e10
Summary: Removing an internal error in SIL to HIL translation which I had added before to log how often the particular case was happening. It happens quite often, and I have a task to investigate the issue. Removing it as it spams the analysis output a lot.
Reviewed By: dulmarod
Differential Revision: D8316822
fbshipit-source-id: 4047cbe
Summary: Introduce an annotation that forces the summary of a method to be free of blocking events, without suppressing other reports.
Reviewed By: jeremydubreil
Differential Revision: D8276787
fbshipit-source-id: be9eed8
Summary: I don't understand what this function is for. Let's remove it.
Reviewed By: mbouaziz
Differential Revision: D8320839
fbshipit-source-id: eeb14f7
Summary: The case of nullable properties was already working but there was no test for it.
Reviewed By: dulmarod
Differential Revision: D8266468
fbshipit-source-id: c074d69
Summary:
`make doc` will use `jbuilder` (which in turn uses `odoc`) to generate the
documentation for infer's modules. This is useful to browse the APIs of infer
and gives a more discoverable place to host more general documentation about
infer's internals.
Besides the actual plumbing necessary to generate the docs, this diff also
- Moves the various infer/src/*/README.md to index.mld files that make it to the generated docs
- Fixes some doc comments that would anger `ocamldoc`
Closes#435
Reviewed By: mbouaziz
Differential Revision: D8314572
fbshipit-source-id: 4a5c70e
Summary: Create mechanism for suppressing starvation reports. To do that, refactor and expose a Checkers function.
Reviewed By: mbouaziz
Differential Revision: D8259583
fbshipit-source-id: f5b5a63
Summary: There is a number of dangling pointer dereference false positives coming from our treatment of union in c/cpp. For now, do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8279802
fbshipit-source-id: a339b0e
Summary: We get a lot of false positives for union types as union fields are treated as separate memory locations at the moment. For now we do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8277363
fbshipit-source-id: efe5b4a
Summary:
Now the result won't depend on the visit order of instructions
Depends on D8235834
Reviewed By: jeremydubreil
Differential Revision: D8235907
fbshipit-source-id: a6eb469
Summary:
Use the component of the abstract state `events` to report. This set contains reachability facts about blocking calls and lock acquisitions.
The other component, `order`, contained pairs of a reachable event `e'` from an event option with the semantics that if the option is `None` then we have an element that now goes into `events`, and if the option is `Some e` then the element represents a lock acquired and a trace *from* `e` to `e'`
Now, `order` can be simplified to proper pairs of events, without the option.
Reviewed By: jvillard
Differential Revision: D8227665
fbshipit-source-id: e6f4dac
Summary:
Having the `Node` module including in the `CFG` one is confusing.
Let's keep it separate.
Reviewed By: ngorogiannis
Differential Revision: D8185754
fbshipit-source-id: 62077e6
Summary:
It's useful to test that the bucket a given error is classified as doesn't
change over time without notice.
This records the bucket for *all* the tests, even though some never produce a
bucket. This is to be on the safe size instead of risking to forget adding the
bucket information when the test changes, or when copy/pasting from a test that
doesn't have buckets to one that does.
The implementation is pretty crude: it greps the beginning of the qualifier
string for a `[bucket]`.
Reviewed By: mbouaziz
Differential Revision: D8236393
fbshipit-source-id: b3b1eb9
Summary: That name doesn't make sense anymore and could be confusing.
Reviewed By: mbouaziz
Differential Revision: D8235507
fbshipit-source-id: b6a6e71
Nikos Gorogiannis
Mehdi Bouaziz
Dulma Churchill
Martino Luca
Daiva Naudziuniene
Dino Distefano
Ezgi Çiçek
Jeremy Dubreil
Jules Villard