Posts for the month of October 2009

Read back serialized test objects

The jpf-core hg:5a95fbcbfda8 change fixes (at least for classes not doing fancy serialization). This might be of interest if you have an SUT that requires very complex test data input, and you want to avoid the effort of creating this in your JPF test driver - serialize it outside JPF and read it back from a file within your JPF run. See for an example

Added @SandBox annotation to jpf-aprop

The jpf-aprop project got a new @SandBox annotation and SandBoxChecker listener. It basically means an object is allowed to change itself, and any non-leaked objects it created, but nothing outside. Details on projects/jpf-aprop/SandBox

This is an interesting scope-based property. It could be the basis for a lot more, e.g. security related properties

Configuration Changes for Randomizing Choices

cg.randomize_choices now has three options: def (default search), random (randomize choices using the system time as seed), and path (randomize choices using a preset or user-specified seed). Please note that any previous scripts users might have setting randomize_choices as boolean values will not work. Please update your properties file and scripts. The details on the on configuration changes are provided here.

Server outage on weekend 10/23-10/25

You won't be able to read this Fri, 10/23 5pm - Sun 10/25, due to some scheduled maintenance work that affects the server. All should be back to normal on Monday, 10/26.

Good thing we use Mercurial, so that you can work offline

Changes potentially affecting existing listeners

hg:83236c926611 of jpf-core has two changes that might affect your listeners:

(1) in addition to the old exceptionThrown(vm), there are new exceptionBailout(vm) and exceptionHandled(vm) notifications. This is mostly to simplify life for listeners that monitor exception handling, but if you have listeners that are not derived from ListenerAdapter or PropertyListenerAdapter, you have to add these methods

(2) ThreadInfo.executeInstruction() has been changed to update the PC after post-exec notification, i.e. instructionExecuted() listeners that rely on ti.getTopFrame().getPC() != vm.getLastInstruction() have to be modified. See the commit message for the rationale.

new ExceptionInjector listener added to jpf-core

There is a new listener gov.nasa.jpf.listener.ExceptionInjector, which can be used to throw user specified exceptions at arbitrary locations. This is helpful to test notoriously under-tested exception handlers, e.g. if it is hard to force a specific exception. The goal is to test exception handlers in simple unit tests.

Details on projects/jpf-core/ExceptionInjector, comments welcome.

Eclipse JPF is now available!

A new plugin for Eclipse has been released named: eclipse-jpf

Main features include:

  • Seamless integration of *.jpf files into Eclipse
  • Source linking of JPF output
  • No more need for messy Eclipse run configurations!