Skip to content
GitLab
    • Why GitLab
    • Pricing
    • Contact Sales
    • Explore
  • Why GitLab
  • Pricing
  • Contact Sales
  • Explore
  • Sign in
  • Get free trial
  • SoSy-Lab SoSy-Lab
  • Software
  • CPAcheckerCPAchecker
  • Issues
  • #398

Value Analysis could use ambiguous Pointers in PointerCPA strengthening

Original issue created by @lemberger on 2018-05-14 at 15:49:34, last modified on 2018-05-14 at 15:49:34


Currently, the value analysis uses information from the PointerCPA about a pointer only, if the pointer can only point to exactly one address. We could improve this so that the value analysis also uses information, if a pointer could point a) to multiple locations or b) to any location.

In the first case, this could significantly increase the state space, though.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking