infer_clone

Commit Graph

Author	SHA1	Message	Date
Nikos Gorogiannis	0255765a54	[starvation] document false positive Summary: Document FP due to imprecision in tracking outer lock release. In a nested `synchronized` block the outer release is not registered by the abstract domain. The reason is that HIL is not resolving what `$bcvarX` is pointing to (in this case to `lockE`). Reported by Andreea Costea. Reviewed By: ezgicicek Differential Revision: D22186240 fbshipit-source-id: 84e5e72b1	5 years ago
Nikos Gorogiannis	0a06353bce	[starvation] more tests documenting interaction with thread status Summary: As per title. These test pass already because the previous thread domain was sufficient to express them. This won't necessarily be true when the whole-program analysis version comes around, because we may decide to not report on the `Threaded` elements (see domain). Reviewed By: dulmarod Differential Revision: D17930653 fbshipit-source-id: 2174f6b22	5 years ago

Author

SHA1

Message

Date

Nikos Gorogiannis

0255765a54

[starvation] document false positive

Summary:
Document FP due to imprecision in tracking outer lock release. In a nested `synchronized` block the outer release is not registered by the abstract domain.  The reason is that HIL is not resolving what `$bcvarX` is pointing to (in this case to `lockE`).

Reported by Andreea Costea.

Reviewed By: ezgicicek

Differential Revision: D22186240

fbshipit-source-id: 84e5e72b1

Nikos Gorogiannis

0a06353bce

[starvation] more tests documenting interaction with thread status

Summary: As per title.  These test pass already because the previous thread domain was sufficient to express them.  This won't necessarily be true when the whole-program analysis version comes around, because we may decide to not report on the `Threaded` elements (see domain).

Reviewed By: dulmarod

Differential Revision: D17930653

fbshipit-source-id: 2174f6b22

2 Commits (debeba5860fe2c97b2dd7e0f7f7a8b8b35000f8c)