Java Ranger is a path-merging extension of Symbolic PathFinder
When considering a new transformation to be added to Java Ranger, you should first ask yourself if this transformation needs to be done exactly once or multiple times as part of a fixed-point computation. If it is a former kind of transformation, then call it from VeritestingListener.runVeritesting. If it is the latter kind of transformation, then call it from FixedPointWrapper.executeFixedPointTransformations. In either case, you will want to add it to the gov.nasa.jpf.symbc.veritesting.ast.transformations package. If the transformation is a static one (changes only the static representation of a region in JR IR), you will want to ensure you call it inside the StaticRegion constructor.
One important point to note for all JR transformations is that every region summary (represented as a Stmt inside StaticRegion or DynamicRegion) is immutable. Please try to maintain this design in new transformations because it helps examine the effect of each transformation on a region summary.
The newly introduced transformation can choose to modify the summary’s state or the summary’s statement. The state refers to the fields contained in the StaticRegion or DynamicRegion whereas the statement refers to the stmt or dynStmt field in these two classes respectively. The state can include
psm)
inputTable and outputTable)varTypeTable)endIns)spfPredicateSummary)SPFCases)arrayOutputs)constantsTable)