Feature #10551
closed
Feature #8119: Develop preset tags
Develop preset tags for CPALockator
Added by Evgeny Novikov over 3 years ago.
Updated over 3 years ago.
Category:
Preset jobs, marks and tags
Description
CPALockator is involved by Klever users more and more. It has rather specific false alarm reasons. As a result of this feature request I expect a subtree of corresponding tags with appropriate descriptions in any suitable form.
Tags are combined from different marking bases:
- Predicate Analysis (Problems with PredicateCPA)
- Memory model (Problems with simple memory model)
- Different structures (Two different instances of the same structure type is considered to be the same object)
- List operations (Operations with list elements usually should considered as operations with the whole list)
- Shared data (Shared data may be considered to have arbitrary values to guarantee soundness of analysis without effects)
- Global infeasibility (Two racy paths are feasible one by one, but contradicts each other in parallel)
- Lock Analysis (Problems with LockCPA)
- Ad-hoc synchronization (Custom synchronization via variables)
- Missed synchronization (The locking function is absent in configuration)
- Interrupts (Specifics of interrupts is not considered)
- Signals (Specifics of signals is not considered)
- Conditional locking (Lock/Unlock operations are conditional, it leads to a set of infeasible paths)
- Protected get (Atomic extraction of a data from shared container, and access to it without locking as to a local one)
- BAM (Problems with BAM CPA)
- Thread Analysis (Problems with ThreadCPA)
- Shared Analysis (Problems with LocalCPA)
- Missed allocation (The allocation function is absent in configuration)
- Shared merge (Shared analysis is path insensitive, it may miss precise information about locality)
- Lightweight mode (Predicate analysis is absent in lightweight mode)
- Auxiliary variables (The race is found for auxiliary variable in non-target code)
- RCU analysis (Problems with RCU analysis)
- Alias analysis (Alias analysis is not precise enough)
- RCU lists (RCU operations over lists are not completely supported)
- Status changed from New to Resolved
I added these tags to preset ones in branch bridge_9396.
- Status changed from Resolved to Closed
I merged this branch to master in 2625e7311 after CI passed test cases. This change is not backward compatible. Moreover, you should migrate your marks manually using preset tags as most as possible.
Also available in: Atom
PDF