javapathfinder-user — usage related topics (installing, running, options, output...)

Re: [Javapathfinder-user] [Javapathfinder-devel] What will be a good point to start

[Arnab D. <arn...@gm...>]

Hi Peter,
Thanks for your reply. I need a little more help.
For my tool, I need to modify the state structure and the transitions
that are possible from the current state. Which classes I should look into?
Is it enough to modify the SystemState class? How changing it affects GC and
POR? Is there any other place I should look into?

Thanks and regards,
Arnab.

On Feb 20, 2008 3:12 PM, Peter C. Mehlitz <Pet...@na...> wrote:

> the core is fairly stable, and changes are always tested against the
> regression tests, so I would recommend going with the SVN head. Most
> of the current work is going on in extensions and the annotations
> i.e. doesn't affect the rest of the system. Changes of the core are
> usually small bug fixes you want to get anyways.
>
> -- Peter
>
>
> On Feb 19, 2008, at 7:15 PM, Arnab De wrote:
>
> > Hi,
> > I'm trying to develop a tool using JPF and for this, I need a
> > stable but recent version of the JPF source code. As lots of
> > developments are going on in JPF, I'm not sure whether the latest
> > checkout from SVN is stable enough! Could you please tell me how to
> > get a clean and stable version of the code? A slightly outdated
> > version will do, but I do not want to used the 2005 version that is
> > given in the download page.
> >
> > Thanks and regards,
> > Arnab.
> >
> > --
> > Arnab De
> > -----------------------------------------------------------
> > Graduate Student.
> > Computer Science and Automation Department,
> > Indian Institute of Science, Bangalore.
> > http://people.csa.iisc.ernet.in/arnabde
> > -----------------------------------------------------------
> > ----------------------------------------------------------------------
> > ---
> > This SF.net email is sponsored by: Microsoft
> > Defy all challenges. Microsoft(R) Visual Studio 2008.
> > http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> > _______________________________________________
> > Javapathfinder-devel mailing list
> > Jav...@li...
> > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
>
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
>



-- 
Arnab De
-----------------------------------------------------------
Graduate Student.
Computer Science and Automation Department,
Indian Institute of Science, Bangalore.
http://people.csa.iisc.ernet.in/arnabde
-----------------------------------------------------------

Re: [Javapathfinder-user] [Javapathfinder-devel] What will be a good point to start

[Peter C. M. <Pet...@na...>]

the core is fairly stable, and changes are always tested against the  
regression tests, so I would recommend going with the SVN head. Most  
of the current work is going on in extensions and the annotations  
i.e. doesn't affect the rest of the system. Changes of the core are  
usually small bug fixes you want to get anyways.

-- Peter 


On Feb 19, 2008, at 7:15 PM, Arnab De wrote:

> Hi,
> I'm trying to develop a tool using JPF and for this, I need a  
> stable but recent version of the JPF source code. As lots of  
> developments are going on in JPF, I'm not sure whether the latest  
> checkout from SVN is stable enough! Could you please tell me how to  
> get a clean and stable version of the code? A slightly outdated  
> version will do, but I do not want to used the 2005 version that is  
> given in the download page.
>
> Thanks and regards,
> Arnab.
>
> -- 
> Arnab De
> -----------------------------------------------------------
> Graduate Student.
> Computer Science and Automation Department,
> Indian Institute of Science, Bangalore.
> http://people.csa.iisc.ernet.in/arnabde
> -----------------------------------------------------------
> ---------------------------------------------------------------------- 
> ---
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ 
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel

[Javapathfinder-user] What will be a good point to start

[Arnab D. <ar...@cs...>]

Hi,
I'm trying to develop a tool using JPF and for this, I need a stable but
recent version of the JPF source code. As lots of developments are going on
in JPF, I'm not sure whether the latest checkout from SVN is stable enough!
Could you please tell me how to get a clean and stable version of the code?
A slightly outdated version will do, but I do not want to used the 2005
version that is given in the download page.

Thanks and regards,
Arnab.

-- 
Arnab De
-----------------------------------------------------------
Graduate Student.
Computer Science and Automation Department,
Indian Institute of Science, Bangalore.
http://people.csa.iisc.ernet.in/arnabde
-----------------------------------------------------------

Re: [Javapathfinder-user] Documentation?

[Peter C. M. <Pet...@na...>]

There is some documentation for the BytecodeFactory in the context of  
an unpublished paper about the new symbolic execution mode. I will  
probably commit this as a new JPF docu page next week. Contact me  
directly if you need it more urgently, but the mechanism isn't too  
complex - it's an AbstractFactory pattern to create JPF Instruction  
objects from BCEL Instruction objects. Your Instruction classes  
mainly have to provide the execute(..) method, which basically  
represents the concrete execution semantics. You can set the concrete  
factory class with the 'vm.insn_factory.class' property. Examples are  
the symbc and symts extensions.

As to the MJI name mangling, Flavio is right. If there is no  
overloading, you can just skip the mangling, even though it's  
slightly less efficient, and I just do it as a matter of good  
practice. Be aware of that GenPeer only generates the stubs for  
'native' methods of the model class, i.e. you have to do this  
manually if you want to intercept a non-native method.

-- Peter



On Feb 14, 2008, at 2:51 AM, Cristobal J. C. wrote:

> Hi,
>
> I have a couple of questions.
>
> First,
>
> I'm using GenPeer and I see that now it have some options. My  
> question is:
>
> There is any diference between use mangled names or not use it?
>
> and Second,
>
> at my work i need all  the information on JPF that can get,
>
> there is a way of access to information about Bytecode Factories?
>
> the browser brings me the following error:
>
> 1. Server: javapathfinder.sourceforge.net
> 2. URL path: /Bytecode_Factories.html
> 3. Error notes: File does not exist: /home/groups/j/ja/ 
> javapathfinder/htdocs/Bytecode_Factories.html
> 4. Error type: 404
> 5. Request method: GET
> 6. Request query string:
> 7. Time: 2008-02-14 02:48:41 PST (1202986121)
>
>
> thanks in advance
>
>
>
> Todo ruedas: información práctica y todo el glamour del mundo del  
> motor. MSN Estilo y Tendencias
> ---------------------------------------------------------------------- 
> ---
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ 
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

Re: [Javapathfinder-user] Documentation?

[Flavio L. <fl...@gm...>]

Dear Cristobal,

I will give a shot a answering the first question.

>  I'm using GenPeer and I see that now it have some options. My question is:
>  There is any diference between use mangled names or not use it?

When you use mangled names the name of the method in the peer encodes
the types of the arguments.
If you do not have overloaded methods in the class you are generating
a peer for, then there is practically no difference.
However, if you have two different overloadings (which satisfy certain
characteristic), then you need to use overloading.

Example:

The class you want to generate a peer for has the following methods:
  void Add(String s);
and
  void Add(Integer i);

If you do not use mangled names they would be mapped to the same
function is the peer, which would not work.
This is because in the peer String and Integer would both be object references.

I hope this is helpful.
Let me know if you have any questions.

Regards,
-Flavio Lerda

>
>  and Second,
>
>  at my work i need all  the information on JPF that can get,
>
>  there is a way of access to information about Bytecode Factories?
>
>  the browser brings me the following error:
>
>  1. Server: javapathfinder.sourceforge.net
> 2. URL path: /Bytecode_Factories.html
> 3. Error notes: File does not exist:
> /home/groups/j/ja/javapathfinder/htdocs/Bytecode_Factories.html
> 4. Error type: 404
> 5. Request method: GET
> 6. Request query string:
> 7. Time: 2008-02-14 02:48:41 PST (1202986121)
>
>
>  thanks in advance
>
>
>
> ________________________________
> Todo ruedas: información práctica y todo el glamour del mundo del motor. MSN
> Estilo y Tendencias
> -------------------------------------------------------------------------
>  This SF.net email is sponsored by: Microsoft
>  Defy all challenges. Microsoft(R) Visual Studio 2008.
>  http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> _______________________________________________
>  Javapathfinder-user mailing list
>  Jav...@li...
>  https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>
>



-- 
Google Talk: fl...@gm...
MSN Messenger: fl...@gm...
Skype: flerda

[Javapathfinder-user] Documentation?

[Cristobal J. C. <kry...@ho...>]

Hi,
 
I have a couple of questions.
 
First, 
 
I'm using GenPeer and I see that now it have some options. My question is:
 
There is any diference between use mangled names or not use it?
 
and Second, 
 
at my work i need all  the information on JPF that can get,  
 
there is a way of access to information about Bytecode Factories?
 
the browser brings me the following error:
 
1. Server: javapathfinder.sourceforge.net2. URL path: /Bytecode_Factories.html3. Error notes: File does not exist: /home/groups/j/ja/javapathfinder/htdocs/Bytecode_Factories.html4. Error type: 4045. Request method: GET6. Request query string: 7. Time: 2008-02-14 02:48:41 PST (1202986121)
 
 
thanks in advance
 
 
_________________________________________________________________
MSN Video. 
http://video.msn.com/?mkt=es-es

[Javapathfinder-user] Reminder JPF Survey

[JA. S. <JA....@st...>]

Dear sir/madam,

I am Jantien Sessink, a student in Computer Science at the Radboud University in Nijmegen, the Netherlands. For my master thesis I am doing research on the usability of Java PathFinder. Therefore I need some information from JPF users. 

I am gathering information on the usefulness and the ease of use of JPF and the features of JPF that influence these two aspects. This information will be used to evaluate which aspect of JPF could be changed in order to increase its usability. To obtain this information, I have put together a questionnaire containing various questions about this subject.

Last week I sent you the questionnaire about the usability of JPF. If you haven’t filled in this survey, I would be very grateful if you would still complete it. You can fill in the questionnaire at the bottom of this email and simply press reply. It will take approximately 10 minutes to answer the questions, the information will not be used outside of this research and the questionnaire results are used anonymously. If you fill in the questionnaire, I will send you a copy of the research outcome. 

Kind regards,

Jantien Sessink
Radboud University
ja....@st...



------------------------------------------------------------------------------------
This questionnaire contains some questions about your experience with Java PathFinder (JPF). All questions in the first half should be answered on a seven-point scale. Please type the answer between the square brackets. The second half contains open questions. It will take approximately 10 minutes to fill in this form.

PART 1

Scale Used:
1	: Strongly Agree
2	: Moderately Agree
3	: Slightly Agree
4	: Neutral
5	: Slightly Disagree
6	: Moderately Disagree
7	: Strongly Disagree

Perceived Usefulness
1. Using JPF improves the quality of software I build.[]
2. JPF enables me to find concurrency issues more quickly.[]
3. Using JPF allows me to find more concurrency problems than would otherwise be possible.[]
4. Overall, I find JPF useful in my job.[]

Perceived Ease of Use
5. I find interacting with JPF easy.[]
6. I find it easy to get JPF to do what I want it to do.[]
7. Learning to operate JPF was easy for me.[]
8. Overall, I find JPF easy to use.[]

Predicted Future Use
9. I predict I will use JPF on a regular basis in the future.[]

PART 2

The following questions are open questions.

JPF features
10. Why do you find JPF useful or not?


11. What needs to be changed/added to JPF to make it more useful according to you?


12. Why do you find JPF easy to use or not?


13. What needs to be changed/added to JPF to make it easier to use according to you?


14. Do you think you have a positive attitude towards new software tools?


General questions
I am a Man/Woman


How old are you?


What is your highest level of education (Bachelor/Master/PhD/Other)


How many years of experience with model checking do you have?


How many years of experience with Java do you have? 


What is your job title?


How long have you been working with JPF?


Where do you use JPF for?


Do you know anyone else who might use JPF, if so, could you forward this email to him/her?


Thank you very much for filling in this questionnaire.
------------------------------------------------------------------------------------

[Javapathfinder-user] JPF workshop 2008 announcement

[Peter C. M. <Pet...@na...>]

Better late than never - we will have a two days workshop on 05/01  
and 05/02 at the Fujitsu campus in Sunnyvale, CA.

Tentative plans are to have "what is being done with JPF"  
presentations the first day, and reserve the second day for general  
and project specific JPF questions, BoF's and whatever might come up.  
Please have a look at the event web page <http:// 
javapathfinder.sourceforge.net/events/workshop-0508.html> and contact  
Peter Mehlitz at <Pet...@na...> if you are interested to  
attend or give a talk.

Hope to see you there

-- the JPF team

[Javapathfinder-user] JPF survey

[JA. S. <JA....@st...>]

Dear sir/madam,

I am Jantien Sessink, a student in Computer Science at the Radboud University in Nijmegen, the Netherlands. For my master thesis I am doing research on the usability of Java PathFinder. Therefore I need some information from JPF users. 

I am gathering information on the usefulness and the ease of use of JPF and the features of JPF that influence these two aspects. This information will be used to evaluate which aspect of JPF could be changed in order to increase its usability. To obtain this information, I have put together a questionnaire containing various questions about this subject.

I would be very grateful if you could help me and fill in the questionnaire at the bottom of this email. It will take approximately 10 minutes to answer the questions, the information will not be used outside of this research and the questionnaire results are used anonymously. If you fill in the questionnaire, I will send you a copy of the research outcome. 

Kind regards,

Jantien Sessink
Radboud University
Ja....@st...


------------------------------------------------------------------------------------
This questionnaire contains some questions about your experience with Java PathFinder (JPF). All questions in the first half should be answered on a seven-point scale. Please type the answer between the square brackets. The second half contains open questions. It will take approximately 10 minutes to fill in this form.

PART 1

Scale Used:
1	: Strongly Agree
2	: Moderately Agree
3	: Slightly Agree
4	: Neutral
5	: Slightly Disagree
6	: Moderately Disagree
7	: Strongly Disagree

Perceived Usefulness
1. Using JPF improves the quality of software I build.[]
2. JPF enables me to find concurrency issues more quickly.[]
3. Using JPF allows me to find more concurrency problems than would otherwise be possible.[]
4. Overall, I find JPF useful in my job.[]

Perceived Ease of Use
5. I find interacting with JPF easy.[]
6. I find it easy to get JPF to do what I want it to do.[]
7. Learning to operate JPF was easy for me.[]
8. Overall, I find JPF easy to use.[]

Predicted Future Use
9. I predict I will use JPF on a regular basis in the future.[]

PART 2

The following questions are open questions.

JPF features
10. Why do you find JPF useful or not?


11. What needs to be changed/added to JPF to make it more useful according to you?


12. Why do you find JPF easy to use or not?


13. What needs to be changed/added to JPF to make it easier to use according to you?


14. Do you think you have a positive attitude towards new software tools?


General questions
I am a Man/Woman


How old are you?


What is your highest level of education (Bachelor/Master/PhD/Other)


How many years of experience with model checking do you have?


How many years of experience with Java do you have? 


What is your job title?


How long have you been working with JPF?


Where do you use JPF for?


Do you know anyone else who might use JPF, if so, could you forward this email to him/her?


Thank you very much for filling in this questionnaire.
------------------------------------------------------------------------------------

[Javapathfinder-user] eclipse plugin

[David F. <da...@cs...>]

Hello,
As part of a European research project on Aspects (
http://www.aosd-europe.net/) we have developed an Eclipse plugin for JPF.
The plug-in adds a debug configuration that runs your program using JPF's
virtual machine. Currently the plugin is a part of the Common Aspect Proof
Environment (CAPE) tool set, but if there is enough interest we may be able
to create a stand alone version.

If you would like to take the plug-in for a test drive please go to

http://www.cs.technion.ac.il/~ssdl/research/cape/

and then follow the link at the left hand side to the download section. The
web site also contains documentation and a few short movies that demonstrate
the plug-in. Currently we require you to fill a form before we deliver
the plug-in, but we hope to make the CAPE fully open source in a short
time.

Thanks,
The Cape team at the Technion.

[Javapathfinder-user] finalization of a thread

[Cristobal J. C. <kry...@ho...>]

Hi,=20
=20
i am trying to finish a thread, i found your method executeMethod(DirectCal=
lStackFrame frame) inside ThreadInfo.java, =20
=20
but i don't know in what way can i use it,
=20
thanks in advance,=20
=20
and Merry Christmas.
_________________________________________________________________
MSN Noticias
http://noticias.msn.es/comunidad.aspx=

[Javapathfinder-user] Patches welcome?

[Jerry J. <log...@gm...>]

I've gone through a series of contortions to package up Javapathfinder
as an RPM for Fedora Linux systems.  In the process, I've generated a
small set of patches for minor issues with the code base.  I was going
to send them via the Sourceforge patch tracking mechanism [1], but I'm
not encouraged that there are year-old patches there that have neither
been applied to the repository nor commented on.  Are patches from
random people you've never heard of [2] welcome?  If so, should they
be sent to this list?

Incidentally, the mailing list links on [3] are broken.

[1] http://sourceforge.net/tracker/?atid=736892&group_id=136825&func=browse
[2] FWIW, I've been an XEmacs developer for about 10 years now, and
have contributed small patches to PVS over the last several years.  A
more in-depth introduction is available upon request. :-)
[3] http://javapathfinder.sourceforge.net/doc/infra.html

Thanks,
-- 
Jerry James
http://loganjerry.googlepages.com/

[Javapathfinder-user] A heuristic search problem

[<jz...@st...>]

Hi,

I am testing this program:


public static void main(String[] args) {
    int x = Verify.random(10);
    int y = 0;
    Verify.interesing(x > 5);
    Verify.boring(x < 5);
    if(x > 5)
        y = 100;
    if(x < 5)
        y = 50;
    System.out.println("x, y: " x + " " + y);
}


and I have configured the search algorithms to be BFS:

search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
search.heuristic.class = gov.nasa.jpf.search.heuristic.BFSHeuristic


I expect the result to look like:
x, y: 6 100
x, y: 7 100
x, y: 8 100
x, y: 9 100
x, y: 10 100
x, y: 5 0
x, y: 1 50
x, y: 2 50
x, y: 3 50
x, y: 4 50

but the result actually is:

x, y: 1 50
x, y: 2 50
x, y: 3 50
x, y: 4 50
x, y: 5 0
x, y: 6 100
x, y: 7 100
x, y: 8 100
x, y: 9 100
x, y: 10 100

It seems that it is still using DFS search heuristics. Can anyone tell me
why?


Thank you.

J. Zhu

[Javapathfinder-user] how to use abstraction

[H CC <hi...@ho...>]

Hello,

Can anybody tell me how to use abstraction in JPF with the example below?

class Demo4 {
    public static void main(String[] args) {
        int x =3D 0;
        int i;
        for(i =3D 0; i < 10; i++) {
            x++;
            //Abstract.addBoolean("B", x =3D=3D 0);
        }
    }
}

I have no idea how can I pass the compilation.


Thanks,
Harold

_________________________________________________________________
Express yourself instantly with MSN Messenger! Download today it's FREE!
http://messenger.msn.click-url.com/go/onm00200471ave/direct/01/=

Re: [Javapathfinder-user] about ChoiceGenerator

[Peter C. M. <Pet...@na...>]

either from the command line (like "+velocity.class=..."), or from  
any of the JPF property files (preferably mode property file, as you  
should try to avoid changing default.properties). Please see the  
"Configuring JPF Runtime Options" page on the website docu.

- Peter


On Dec 13, 2007, at 1:39 PM, H CC wrote:

> Hello, from  http://javapathfinder.sourceforge.net/doc/ 
> ChoiceGenerators.html (ChoiceGenerator),
> we can see an example:
>
> double v = Verify.getDouble("velocity");
>
> and "velocity" can be configured by:
>
> velocity.class = gov.nasa.jpf.jvm.choice.DoubleThreholdGenerator
> velocity.threhold = 13250
> velocity.delta = 500
>
> but can anyone tell me where we can do the configuration, and show  
> me a simple example.
>
> Thank you.
>
> Harold
>
> Express yourself instantly with MSN Messenger! MSN Messenger
> ---------------------------------------------------------------------- 
> ---
> SF.Net email is sponsored by:
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services
> for just about anything Open Source.
> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/ 
> marketplace_______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

[Javapathfinder-user] about ChoiceGenerator

[H CC <hi...@ho...>]

Hello, from  http://javapathfinder.sourceforge.net/doc/ChoiceGenerators.htm=
l (ChoiceGenerator),
we can see an example:

double v =3D Verify.getDouble("velocity");

and "velocity" can be configured by:

velocity.class =3D gov.nasa.jpf.jvm.choice.DoubleThreholdGenerator
velocity.threhold =3D 13250
velocity.delta =3D 500

but can anyone tell me where we can do the configuration, and show me a sim=
ple example.

Thank you.

Harold

_________________________________________________________________
Express yourself instantly with MSN Messenger! Download today it's FREE!
http://messenger.msn.click-url.com/go/onm00200471ave/direct/01/=

[Javapathfinder-user] Symbolic execution documentation updated

[ciogeetaa j. <tay...@ya...>]

I've checked in some more updates to the documentation for the symbolic execution extension (extensions/symbc/doc/index.html and extensions/symbc/doc/index.pdf).

I'll be adding a bit more to it over the next few days, so any suggestions or corrections are welcome.

David Bushnell


 Send instant messages to your online friends http://uk.messenger.yahoo.com 

Re: [Javapathfinder-user] BUG: Too rigorously POR on array operations (Test model included)

[Viet Y. N. <v.y...@al...>]

Peter Mehlitz schreef:

> P.S. nice to finally see a JPF counterpart for .NET

BTW, I overread this in your previous mail. Just want to let you know, 
the principal designer of MMC (my predecessor), actually used JPF's 
architecture as a reference, and MMC is in fact quite similar to JPF.

The reason why this is so: never change something that works well :)

I am the current author of MMC, and at the end of this month, I will 
release a new version, with improved instruction coverage, stateful 
dynamic POR, POR using object escape analysis, a memoised garbage 
collector (that replaces the traditional mark & sweep), and a collapser 
for the metadata that is kept by stateful dynamic POR.

Viet Yen

Re: [Javapathfinder-user] BUG: Too rigorously POR on array operations (Test model included)

[Viet Y. N. <v.y...@al...>]

Peter Mehlitz schreef:

Thanks for your fast reply!

I have investigated this thoroughly this weekend, and the POR 
optimisation is allowed under certain conditions and assumptions.

The example I sent contains a race, thus it is incorrectly synchronised 
(as defined by the Java Memory Model). That is why arr[0] += 1; cannot 
be seen atomicly.

The POR optimisation is however allowed if you state/assume that JPF 
only verifies a program correctly iff it is correctly synchronised, and 
also state/assume that you only can synchronise statement blocks (thus 
not at the granularity of a JVM bytecode). This ensures sequentially 
consistent semantics of the statements, and thus also the atomicity 
statement arr[0] += 1;

Yet, such Java Memory Model issues are delicate to deal with. It is 
better to bet safe, and assume that an array operation is scheduling 
irrelevant if the array in question is thread-local. Otherwise, the 
array operation should be considered scheduling relevant.

With regards,

Viet Yen



> Thanks - you are right. I guess the comment in 
> ArrayInstruction.isNewPorBoundary(..) was just wishful thinking. If you 
> restore the commented out check, JPF finds the assertion. So it has to 
> go in again, but I want to give it some more thoughts about performance
> 
> -- Peter
> 
> P.S. nice to finally see a JPF counterpart for .NET
> 
> On Dec 3, 2007, at 1:34 AM, Viet Yen Nguyen wrote:
> 
>> Hi,
>>
>> While testing our own model checker 
>> (http://www.cs.utwente.nl/~ruys/mmc/), I discovered, what I believe, 
>> is a bug in yours. The attached model has assertion violations, but 
>> JPF does not find them.
>>
>> It is a POR bug in JPF, as JPF considers array operations as 
>> scheduling irrelevant on the assumption that an array operation is 
>> always preceded by a getfield/getstatic, which is scheduling relevant. 
>> This is not true.
>>
>> Below is a trace to the undetected assertion violation.
>>
>> Could you please verify this bug?
>>
>> With regards,
>>
>> Viet Yen
>>
>>
>>
>> Trace to assertion violation:
>>
>> t1: getfield arr     (gets reference to arr)
>> t2: getfield arr    (gets reference to arr)   
>> t1: iaload          (loads 0 from arr)
>> t1: iadd        (adds 1, result is 1 on t1's stack)       
>> t2: iaload        (loads 0 from arr)
>> t2: iadd        (adds 1, result is 1 on t2's stack)       
>> t1: iastore        (stores 1 to arr)
>> t2: iastore        (stores 1 to arr)
>> t0: check assertion
>> public class TestMArr implements Runnable {
>>
>>     public static int[] arr = new int[1];
>>            
>>     public static void main(String[] args) {
>>         arr[0] = 0;
>>
>>         Thread t1 = new Thread(new TestMArr());
>>         t1.start();
>>
>>         Thread t2 = new Thread(new TestMArr());
>>         t2.start();
>>            
>>         try {
>>             t1.join();
>>             t2.join();
>>         } catch (Exception e) {
>>         }
>>
>>         System.out.println(arr[0]);   
>>         assert(arr[0] == 2);
>>
>>     }
>>     
>>     public void run() {
>>         arr[0] += 1;
>>     }
>> }
>> -------------------------------------------------------------------------
>> SF.Net email is sponsored by: The Future of Linux Business White Paper
>> from Novell.  From the desktop to the data center, Linux is going
>> mainstream.  Let it simplify your IT future.
>> http://altfarm.mediaplex.com/ad/ck/8857-50307-18918-4_______________________________________________ 
>>
>> Javapathfinder-user mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
> 
> ---------------------------------------------------------------------
> Peter C. Mehlitz                    Robust Software Engineering Group
> PSGS/NASA Ames Research Center               Pet...@na...
> M/S 269-3                       http://ti.arc.nasa.gov/people/mehlitz
> Moffett Field, CA 94035                                (650) 604-1682
> 
> 
> 
> 

Re: [Javapathfinder-user] BUG: Too rigorously POR on array operations (Test model included)

[Peter M. <Pet...@na...>]

Thanks - you are right. I guess the comment in  
ArrayInstruction.isNewPorBoundary(..) was just wishful thinking. If  
you restore the commented out check, JPF finds the assertion. So it  
has to go in again, but I want to give it some more thoughts about  
performance

-- Peter

P.S. nice to finally see a JPF counterpart for .NET

On Dec 3, 2007, at 1:34 AM, Viet Yen Nguyen wrote:

> Hi,
>
> While testing our own model checker (http://www.cs.utwente.nl/~ruys/ 
> mmc/), I discovered, what I believe, is a bug in yours. The  
> attached model has assertion violations, but JPF does not find them.
>
> It is a POR bug in JPF, as JPF considers array operations as  
> scheduling irrelevant on the assumption that an array operation is  
> always preceded by a getfield/getstatic, which is scheduling  
> relevant. This is not true.
>
> Below is a trace to the undetected assertion violation.
>
> Could you please verify this bug?
>
> With regards,
>
> Viet Yen
>
>
>
> Trace to assertion violation:
>
> t1: getfield arr 	(gets reference to arr)
> t2: getfield arr	(gets reference to arr)	
> t1: iaload  		(loads 0 from arr)
> t1: iadd		(adds 1, result is 1 on t1's stack)		
> t2: iaload		(loads 0 from arr)
> t2: iadd		(adds 1, result is 1 on t2's stack)		
> t1: iastore		(stores 1 to arr)
> t2: iastore		(stores 1 to arr)
> t0: check assertion
> public class TestMArr implements Runnable {
>
> 	public static int[] arr = new int[1];
> 			
> 	public static void main(String[] args) {
> 		arr[0] = 0;
>
> 		Thread t1 = new Thread(new TestMArr());
> 		t1.start();
>
> 		Thread t2 = new Thread(new TestMArr());
> 		t2.start();
> 			
> 		try {
> 			t1.join();
> 			t2.join();
> 		} catch (Exception e) {
> 		}
>
> 		System.out.println(arr[0]);	
> 		assert(arr[0] == 2);
>
> 	}
> 	
> 	public void run() {
> 		arr[0] += 1;
> 	}
> }
> ---------------------------------------------------------------------- 
> ---
> SF.Net email is sponsored by: The Future of Linux Business White Paper
> from Novell.  From the desktop to the data center, Linux is going
> mainstream.  Let it simplify your IT future.
> http://altfarm.mediaplex.com/ad/ck/ 
> 8857-50307-18918-4_______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

---------------------------------------------------------------------
Peter C. Mehlitz                    Robust Software Engineering Group
PSGS/NASA Ames Research Center               Pet...@na...
M/S 269-3                       http://ti.arc.nasa.gov/people/mehlitz
Moffett Field, CA 94035                                (650) 604-1682

[Javapathfinder-user] BUG: Too rigorously POR on array operations (Test model included)

[Viet Y. N. <v.y...@al...>]

Hi,

While testing our own model checker 
(http://www.cs.utwente.nl/~ruys/mmc/), I discovered, what I believe, is 
a bug in yours. The attached model has assertion violations, but JPF 
does not find them.

It is a POR bug in JPF, as JPF considers array operations as scheduling 
irrelevant on the assumption that an array operation is always preceded 
by a getfield/getstatic, which is scheduling relevant. This is not true.

Below is a trace to the undetected assertion violation.

Could you please verify this bug?

With regards,

Viet Yen



Trace to assertion violation:

t1: getfield arr 	(gets reference to arr)
t2: getfield arr	(gets reference to arr)	
t1: iaload  		(loads 0 from arr)
t1: iadd		(adds 1, result is 1 on t1's stack)		
t2: iaload		(loads 0 from arr)
t2: iadd		(adds 1, result is 1 on t2's stack)		
t1: iastore		(stores 1 to arr)
t2: iastore		(stores 1 to arr)
t0: check assertion

[Javapathfinder-user] JPF Symbolic execution extension

[Pasareanu, Corina S. (ARC-TI)[Q. G. INC] <cor...@na...>]

The JPF symbolic execution extension is called "symbc".
I put some very preliminary documentation in "symbc/doc".

Corina

[Javapathfinder-user] JPF Symbolic execution extension

[Francesco V. <Fra...@ce...>]

Hello,=20
I'm starting to use JPF and I would really like to try the symbolic =
execution extension that comes in the symbc folder. I compiled it and I =
changed the default.properties file in order to use the =
gov.nasa.jpf.symbc.SymbolicInstructionFactory class as instruction =
factory, anyway when I run JPF I get the following error:=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search started: 19/11/07=20
19.38=20
[SEVERE] JPF exception, terminating: class =
java.lang.NullPointerException: null=20
=20
=20
I couldn't find any tutorial on how exactly to use this extension. Can =
anyone give me some help?? =20
=20
Many Thanks,=20
=20
F. Valentini.=20

Re: [Javapathfinder-user] Bug in JPF or in my code?????

[Jantien S. <jan...@gx...>]

Hi,

Is there something known yet about the issue I sent last week? Is JPF
inconsistent with my JVM or is the problem in my code?

Kind regards,
Jantien Sessink=20


-----Original Message-----
From: jav...@li...
[mailto:jav...@li...] On Behalf Of
Jantien Sessink
Sent: Wednesday, October 10, 2007 8:52 AM
To: jav...@li...
Subject: Re: [Javapathfinder-user] Bug in JPF or in my code?????

Hi,

I'm using the same compiler from jdk 1.5.0_12. The map is the standard
Map interface from java.util and the HashMap implementation class.
I wrote some unit tests for JPF to see if Map is supported, and all unit
tests are passed, also the equal function seemed to work ok. I've put
the unit tests in the attachment of this mail.

Kind regards,
Jantien Sessink



-----Original Message-----
From: jav...@li...
[mailto:jav...@li...] On Behalf Of
Peter C. Mehlitz
Sent: Tuesday, October 09, 2007 8:44 PM
To: jav...@li...
Subject: Re: [Javapathfinder-user] Bug in JPF or in my code?????

what kind of map is this (HashMap, type parameters)? One thing could =20
be that the hashcode() or equals() implementation differs between our =20
lib model and the host VM.

-- Peter

------------------------------------------------------------------------
-
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems?  Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
Javapathfinder-user mailing list
Jav...@li...
https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

Re: [Javapathfinder-user] Bug in JPF or in my code?????

[Jantien S. <jan...@gx...>]

Hi,

I'm using the same compiler from jdk 1.5.0_12. The map is the standard
Map interface from java.util and the HashMap implementation class.
I wrote some unit tests for JPF to see if Map is supported, and all unit
tests are passed, also the equal function seemed to work ok. I've put
the unit tests in the attachment of this mail.

Kind regards,
Jantien Sessink



-----Original Message-----
From: jav...@li...
[mailto:jav...@li...] On Behalf Of
Peter C. Mehlitz
Sent: Tuesday, October 09, 2007 8:44 PM
To: jav...@li...
Subject: Re: [Javapathfinder-user] Bug in JPF or in my code?????

what kind of map is this (HashMap, type parameters)? One thing could =20
be that the hashcode() or equals() implementation differs between our =20
lib model and the host VM.

-- Peter

------------------------------------------------------------------------
-
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems?  Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
Javapathfinder-user mailing list
Jav...@li...
https://lists.sourceforge.net/lists/listinfo/javapathfinder-user