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

[Corina P. <Cor...@na...>]

Hello:

I assume you want to add array support in Symbolic JPF (i.e. JPF's symbc 
extension).
That would be a good thing to do :)
For a start, you may want to take a look at the following paper, that 
describes briefly the array support in our old version of symbolic 
execution:

Verification of Java Programs using Symbolic Execution and Invariant 
Generation <http://ti.arc.nasa.gov/m/profile/pcorina/papers/spin04.ps>, 
/Corina S. Pasareanu, Willem Visser/, in Proceedings of the the 11th 
International SPIN Workshop on Model Checking of Software, 2004.

With the techniques described above, you don't need array logic support 
in the decision procedure.

Best regards,
Corina


jiangfan shi wrote:
> 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
>
> ------------------------------------------------------------------------
>
> ------------------------------------------------------------------------------
> This SF.net email is sponsored by:
> SourcForge Community
> SourceForge wants to tell your story.
> http://p.sf.net/sfu/sf-spreadtheword
> ------------------------------------------------------------------------
>
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>   


-- 
Corina Pasareanu, PhD
CMU/NASA Ames
http://ti.arc.nasa.gov/profile/pcorina/