[Javapathfinder-user] one question about array support in JPF

[jiangfan s. <jia...@gm...>]

Hello, Corina,

I am trying to add a very heuristic support for the array type due to my
research requirement. I found there is a package named
gov.nasa.jpf.symbolic.array, which includes some array related classes, such
as ArrayIntStructure.java, ArrayBoolStructure.java.

I have two understandings here, and I wonder if they are right or not.


   1. The ArrayIntStructure class is a symbolic representation of array type
   via a vector, and it fulfills an array logic including read and write
   axioms, via to its' associated operations including set and get methods.
   2. What I need to do for supporting array in JPF is the following:
      - call ArrayIntStructure constructor to do an array type
      initialization from the execute() method of BytecodesUtils.java
      - for every operators, such as add, minus, load, ifle etc., I need to
      check if an operand is an array type, and if so, call set or get
methods in
      ArrayIntStructure class.
      - finally I need to transform some array-related path conditions to
      the format which is consistent with cvc3 or other decision procedures
      supporting array logic. I should do this in the
SymbolicConstraintsGeneral
      class.

Am I right for these two understandings?

Thanks in advance, and any hint is highly appreciated!

Jiangfan