Skip to content

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