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

Query regarding lazy initialization and polymorphic fields/inputs #27

Closed unshorn closed 4 years ago

unshorn commented 5 years ago

Hi, I would like to clarify this message which I get when I try to run jbse on a method that takes a type with a field that might resolve to multiple concrete types. The message I get is : .1.1 {ROOT}:c.property not expanded. It may be a hint of too strong user-defined constraints, possibly correct when enforcing redundancy by representation invariant.

In one implementation of a method in the object that c.property may point to, I am expecting it to produce an unsafe trace. How can I get the engine to expand the field to all possible types?