Wrong resolution of symbolic references: no alias to static members
pietrobraione opened this issue · 1 comments
Even when some classes are assumed to be pre-initialized, it may happens that their static class members are not initialized symbolically but by running the concrete static initializer. This happens, e.g., when a class has a pure static initializer. This means that there is no resolution clause for these members in the path condition. Therefore, there is no hope that any other symbolic reference is resolved as alias to these members.
Commit 3656618 introduces the possibility of making the pre-initial classes symbolic. This is controlled by the parameter method setMakePreInitClassesSymbolic(boolean). Beware that, when activated this option, the state space may explode because all the objects stored in static fields (and recursively) of classes created during VM bootstrap become potential aliases!