Report Bugs, when run testgen
Marvinmw opened this issue · 2 comments
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)
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.
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.