Attributes

JPF uses attributes this way:

While JPF stores values for operands, local variables and fields very similar to a normal VM, it also features a storage extension mechanism that lets you associate arbitrary objects with stack slots (operands and locals), fields, and whole objects (ElementInfos). The attribute objects can be set/used in native peers or listeners to add state stored/restored information that automatically follows the data flow.

The most well-known module that uses attributes is jpf-symbc (see below).

The Inspector allows you to read and set attributes associated with fields and local variables via the commands set_attr, print_attr and via the hit conditions attr_access, attr_write and attr_read.

For more general information on attributes, see:

• http://babelfish.arc.nasa.gov/trac/jpf/wiki/devel/attributes

Reading attributes

Attribute values are displayed using the command print and in the visual Explorer. See the documentation for print for more details.

Attribute values are normally printed using their toString() methods but it is possible to override this (see Attributes (extensibility)).

Setting new attribute values

It is possible to set or change the attribute of an object while the program is paused. For example, you may use

set_attr this.fieldInt = 4

to set the attribute of the field fieldInt to a symbolic IntegerConstant with the value 4 (if you have jpf-symbc loaded).

To convert strings that are the arguments of set_attr to actual attribute objects, converters are used. See set_attr and Attributes (extensibility) for details.

jpf-symbc

JPF Inspector comes packaged with attribute adaptors for the module jpf-symbc which adds symbolic execution support to Pathfinder.

To set up this support, see Attributes (SPF).

Attributes associated with ElementInfo objects

The Inspector does not allow the user to read or modify attributes stored with ElementInfo objects themselves, only attributes stored with the relationships, i.e. fields, stack slots and array elements.

As far as we know, there is no public JPF module that makes use of attributes associated directly with ElementInfo objects.

Multiple attributes

JPF supports multiple attributes for each object or relationship (source). However, modules developed before this features was implemented, such as jpf-symbc, still expect that there is only a single attribute for each field or element.

JPF Inspector supports multiple attributes partially: It will print out the values of all attributes, but when you set an attribute, all existing attributes are erased and replaced with the new, single, attribute.

Original specification

The original specification document for this features is this:

• https://docs.google.com/document/d/1cTVZRCmWKgQJLdjSH9N-dl-lSh83e6gR8p3rS5wiC2o/edit