Klever

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)