Project

General

Profile

Feature #10551

Feature #8119: Develop preset tags

Develop preset tags for CPALockator

Added by Evgeny Novikov 3 months ago. Updated about 1 month ago.

Status:
Closed
Priority:
Urgent
Category:
Preset jobs, marks and tags
Target version:
Start date:
10/21/2020
Due date:
% Done:

0%

Estimated time:
Published in build:

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.

History

#1

Updated by Pavel Andrianov 3 months ago

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)
#2

Updated by Evgeny Novikov about 1 month ago

  • Status changed from New to Resolved

I added these tags to preset ones in branch bridge_9396.

#3

Updated by Evgeny Novikov about 1 month ago

  • 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