search

pietrobraione / jbse

A symbolic Java virtual machine for program analysis, verification and test generation
http://pietrobraione.github.io/jbse/
GNU General Public License v3.0
101 stars 29 forks source link

Wrong resolution of symbolic references: no alias to static members #23

Closed pietrobraione closed 5 years ago

pietrobraione commented 5 years ago

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.

pietrobraione commented 5 years ago

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!