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

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

Thanks very much, Corina.

I would like to read this paper again more carefully first,  modify my
procedure to extend the JPF-SE to support array in my last email, and then
send it back to you to check if the procedure is right or not.

Best,

Jiangfan

On Thu, Jan 22, 2009 at 1:56 PM, Corina Pasareanu <
Cor...@na...> wrote:

> 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/
>