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
103 stars 29 forks source link

Too much Output #24

Closed spyyes closed 5 years ago

spyyes commented 5 years ago

Hi, I'm a new starter of jbse. When I run the basic example -- IfExample, the output was extremely long (I attached the file in my appendix). I tried to figure out that this due to too many variables and structures from the external libraries. Could you please tell me whether there are configurations to filter them out?

runIf_z3.txt

pietrobraione commented 5 years ago

Hi, I have changed some defaults, now the output is shorter. In general, if you set p.setStateFormatMode(StateFormatMode.FULLTEXT) instead of p.setStateFormatMode(StateFormatMode.TEXT) you will have a longer output. Same if you set p.setMakePreInitClassesSymbolic(true), that is not really a useful option if you do not use JBSE for generating test cases (I turned it on by default before I decided that it is better to leave it off by default).