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

Report Bugs, when run testgen #26

Open Marvinmw opened 5 years ago

Marvinmw commented 5 years ago

Exception in thread "main" java.lang.ClassCastException: jbse.mem.ClauseAssumeNull cannot be cast to jbse.mem.ClauseAssume at jbse.apps.StateFormatterJUnitTestSuite$JUnitTestCase.setWithNewObject(StateFormatterJUnitTestSuite.java:461) at jbse.apps.StateFormatterJUnitTestSuite$JUnitTestCase.appendInputsInitialization(StateFormatterJUnitTestSuite.java:281) at jbse.apps.StateFormatterJUnitTestSuite$JUnitTestCase.(StateFormatterJUnitTestSuite.java:238) at jbse.apps.StateFormatterJUnitTestSuite.formatState(StateFormatterJUnitTestSuite.java:77) at jbse.apps.run.Run.emitState(Run.java:1042) at jbse.apps.run.Run.access$3(Run.java:1040) at jbse.apps.run.Run$ActionsRun.atTraceEnd(Run.java:425) at jbse.jvm.Runner.doRun(Runner.java:612) at jbse.jvm.Runner.run(Runner.java:520) at jbse.apps.run.Run.run(Run.java:584) at testgen.RunTestgen.main(RunTestgen.java:16)

pietrobraione commented 5 years ago

The JUnit test suite state formatter is lagging behind the last developments of JBSE and it is really a toy. I will decide whether to fix it or just to retire it. If you want to use JBSE to generate tests please try SUSHI or TARDIS.

pietrobraione commented 5 years ago

The bug is caused by the fact that, when the pre-initial classes are (pedantically) made symbolic via the suitable JBSE parameter, it is no longer true the invariant that in all path conditions, after an expansion clause to an array, there is a clause predicating on the array length. This is true for the classes that are created after the initialization, but not for the pre-initial classes that are made symbolic. The bug can be solved by making the state formatter skip all the pre-initial path condition clauses (on which we cannot do anything anyways). Commit da28cab of JBSE changes the default of making pre-initial classes symbolic to not making them, so if you use the latest version of JBSE the exception is no longer thrown and everything works again.