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

[Javapathfinder-user] I can"t run JPF

[En Ye <ye....@gm...>]

Hi all,

After I ran the "ant run-tests" command successfully, I tried to use
JPF to model check the HelloWorld application in the example
directory, however,  I cannot get it to work.
When I ran the jpf.bat in WindowXP, I encountered the error as following:
D:\javapathfinder>bin\jpf.bat HelloWorld
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames
Research Center
JPF exception, terminating: could not load class D:\javapathfinder\bin\..\b=
uild\
env\jpf;
When I ran the jpf in Linux, I encountered the error as following:
$ bin/jpf HelloWorld
: bad interpreter: No such file or directory
The jdk version I used is 1.4.2.=20
I can"t  figure out the error. So could someone give me some advice?
Thanks in advance.

Yearn

Re: [Javapathfinder-user] Running JPF

[Martijn H. <M.H...@cs...>]

Hi Peter,

Thanks for your reply, it makes things more clear, and I can use jpf now!

Best wishes,

Martijn

Peter C. Mehlitz wrote:
> You have to start jpf like a normal VM, i.e. you give it a class  name, 
> NOT the classfile. That means, this class has to be either in  the 
> classpath, or in the path that's used only by JPF to load classes  
> (+vm.classpath), i.e. which are not seen by the host VM.
> 
> In you first example, the problem is simply that you have to specify  
> the classname (the ./examples dir is already set in the classpath by  
> the bin/jpf script):
> 
>   > bin/jpf HelloWorld
> 
> In your second example, the problem is that jpf - before it would not  
> have found HelloWorld - doesn't find it's native peer model classes  
> anymore (the MJI stuff in build/env/jpf), like java.lang.Thread and  
> others. Please read the MJI docu section for that - model classes  have 
> to be ONLY in the vm.classpath (the host VM shouldn't see them  because 
> it needs the real java.lang.Thread etc.), the native peers  have to be 
> in the CLASSPATH (to make sure the host VM finds them). A  bit 
> confusing, but think of jpf as a JVM that is running on top of a  JVM.
> 
> -- Peter
> On Aug 5, 2005, at 2:49 AM, Martijn Hendriks wrote:
> 
>> Hi,
>>
>> I am new to JPF and I am trying to modelcheck the HelloWorld app in  
>> the example directory. I just cannot get it to work:
>>
>> javapathfinder > bin/jpf examples/HelloWorld.class
>> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA  Ames 
>> Research Center
>> JPF exception, terminating: could not load class  
>> examples.HelloWorld.class
>>
>> examples > ../bin/jpf HelloWorld.class
>> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA  Ames 
>> Research Center
>> error during VM runtime initialization: wrong model classes (check  
>> vm.[boot]classpath)
>>
>> and i tried a lot more... I probably need to set some paths, but I  
>> can't figure what to do exactly.
>>
>> The "ant run-tests" works fine: no errors are reported (I am using  
>> j2sdk1.4.2_08 on Linux).
>>
>> It would be great if someone could help me with this.
>>
>> Thanks!
>>
>> Martijn Hendriks
> 
> 
> 
> -------------------------------------------------------
> SF.Net email is Sponsored by the Better Software Conference & EXPO
> September 19-22, 2005 * San Francisco, CA * Development Lifecycle Practices
> Agile & Plan-Driven Development * Managing Projects & Teams * Testing & QA
> Security * Process Improvement & Measurement * http://www.sqe.com/bsce5sf
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

Re: [Javapathfinder-user] Running JPF

[Peter C. M. <pcm...@em...>]

You have to start jpf like a normal VM, i.e. you give it a class  
name, NOT the classfile. That means, this class has to be either in  
the classpath, or in the path that's used only by JPF to load classes  
(+vm.classpath), i.e. which are not seen by the host VM.

In you first example, the problem is simply that you have to specify  
the classname (the ./examples dir is already set in the classpath by  
the bin/jpf script):

   > bin/jpf HelloWorld

In your second example, the problem is that jpf - before it would not  
have found HelloWorld - doesn't find it's native peer model classes  
anymore (the MJI stuff in build/env/jpf), like java.lang.Thread and  
others. Please read the MJI docu section for that - model classes  
have to be ONLY in the vm.classpath (the host VM shouldn't see them  
because it needs the real java.lang.Thread etc.), the native peers  
have to be in the CLASSPATH (to make sure the host VM finds them). A  
bit confusing, but think of jpf as a JVM that is running on top of a  
JVM.

-- Peter 

On Aug 5, 2005, at 2:49 AM, Martijn Hendriks wrote:

> Hi,
>
> I am new to JPF and I am trying to modelcheck the HelloWorld app in  
> the example directory. I just cannot get it to work:
>
> javapathfinder > bin/jpf examples/HelloWorld.class
> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA  
> Ames Research Center
> JPF exception, terminating: could not load class  
> examples.HelloWorld.class
>
> examples > ../bin/jpf HelloWorld.class
> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA  
> Ames Research Center
> error during VM runtime initialization: wrong model classes (check  
> vm.[boot]classpath)
>
> and i tried a lot more... I probably need to set some paths, but I  
> can't figure what to do exactly.
>
> The "ant run-tests" works fine: no errors are reported (I am using  
> j2sdk1.4.2_08 on Linux).
>
> It would be great if someone could help me with this.
>
> Thanks!
>
> Martijn Hendriks

[Javapathfinder-user] Running JPF

[Martijn H. <mar...@cs...>]

Hi,

I am new to JPF and I am trying to modelcheck the HelloWorld app in the 
example directory. I just cannot get it to work:

javapathfinder > bin/jpf examples/HelloWorld.class
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames 
Research Center
JPF exception, terminating: could not load class examples.HelloWorld.class

examples > ../bin/jpf HelloWorld.class
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames 
Research Center
error during VM runtime initialization: wrong model classes (check 
vm.[boot]classpath)

and i tried a lot more... I probably need to set some paths, but I can't 
figure what to do exactly.

The "ant run-tests" works fine: no errors are reported (I am using 
j2sdk1.4.2_08 on Linux).

It would be great if someone could help me with this.

Thanks!

Martijn Hendriks

Re: [Javapathfinder-user] Array of Double Question

[Peter C. M. <pcm...@em...>]

Outch! Index screwup in ElementInfo.get/setLongElement(), no idea how  
this sneaked in. The index values in Fields are int[] based, so the  
ElementInfo methods have to be adjusted *2:

   public void setLongElement(int index, long value) {
     checkArray(index);
     cloneFields().setLongValue(index*2, value);
   }

   public long getLongElement(int index) {
     checkArray(index);
     return fields.getLongValue(index*2);
   }

It's committed, but as always it takes a while until this shows up in  
the public CVS

-- Peter



On Jul 29, 2005, at 1:08 PM, Chiu C. Tan wrote:


> Hi
>
> I experimenting with Java Pathfinder for a class and came across a
> strange behaviour.
> In a nutshell, I have an array of 4 doubles, [0.0, 1.0, 2.0, 3.0]  
> and I
> want to swap the first element with the
> third element. So the final result should be [0.0, 3.0, 2.0, 1.0].
>
> However, running this simple code through jpf shows that after the  
> swap,
> the array becomes
> [0.0, 3.0, 0.0, 1.0]
>
> (The actual values are a little different, I just rounded them up for
> clarity.)
> Does anyone have an explanation for this?
>
> Thanks
> Chiu
>

[Javapathfinder-user] Array of Double Question

[Chiu C. T. <cc...@cs...>]

Hi

I experimenting with Java Pathfinder for a class and came across a
strange behaviour.
In a nutshell, I have an array of 4 doubles, [0.0, 1.0, 2.0, 3.0] and I
want to swap the first element with the
third element. So the final result should be [0.0, 3.0, 2.0, 1.0].

However, running this simple code through jpf shows that after the swap,
the array becomes
[0.0, 3.0, 0.0, 1.0]

(The actual values are a little different, I just rounded them up for
clarity.)
Does anyone have an explanation for this?

Thanks
Chiu



I have attached a copy of the code and the output below.

--------------------------------------------------------------------------
Code:
import gov.nasa.jpf.jvm.Verify;
import java.util.Random;

public class Swap {

    public static void main (String[] args) {
        double[] numbers;
        numbers = new double[4];

        numbers[0] = 0.0;
        numbers[1] = 1.0;
        numbers[2] = 2.0;
        numbers[3] = 3.0;

        Verify.instrumentPoint("pre-sort");

System.out.print("1) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        double t = numbers[1];

System.out.print("t is "+t+"\n");
System.out.print("2) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        numbers[1] = numbers[3];

System.out.print("3) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        numbers[3] = t;

System.out.print("numbers[1] is "+numbers[1]+" and numbers[3] is
"+numbers[3]+"\n");
System.out.print("4) "+numbers[0] + ", " + numbers[1] + ", " +
numbers[2] + ", " + numbers[3] +"\n\n");

        Verify.instrumentPoint("post-sort");

System.out.print("After\n");
System.out.print(numbers[0] + ", " + numbers[1] + ", " + numbers[2] + ",
" + numbers[3] +"\n\n");
    }
}
-------------------------------------------------------------------------------------------------------------

Output:

Java Pathfinder Model Checker v3.1.2 - (C) 1999-2005 RIACS/NASA Ames
Research Center
1) 5.299808824E-315, 1.000000238418579, 2.000000477069989, 3.0

t is 1.000000238418579
2) 5.299808824E-315, 1.000000238418579, 2.000000477069989, 3.0

3) 5.307579804E-315, 3.0, 5.307579804E-315, 3.0

numbers[1] is 3.0 and numbers[3] is 1.000000238418579
4) 5.307579804E-315, 3.0, 5.299808824E-315, 1.000000238418579

After
5.307579804E-315, 3.0, 5.299808824E-315, 1.000000238418579

------------------------------------ thread stacks
Thread: main
        at Swap.main(Swap.java:8)

------------------------------------ end thread stacks


===================================
  No Errors Found
===================================

[Javapathfinder-user] Re: JPF for Methods?

[Muhammad A. S. <muh...@gm...>]

Ok, here is my reply. Please correct me if I am wrong.

Currently you have to write instrumentation code; to exhaustively test
everything, use Verify.random() for generating integers and booleans.
The same code can be rewritten as follows:

import gov.nasa.jpf.jvm.Verify;

public class MaxWhile {
    public static int findMax (int []a) {
=09int k =3D 1;
=09int max =3D a[1];

=09while (k < a.length) {
=09    if (a[k] > max) max =3D a[k];
=09    k++;
=09}

=09return max;
    }

    public static void main (String args[]) {
=09int [] myArray =3D new int [Verify.random(10)];
=09if (myArray.length <=3D 1) return;

=09for (int i=3D0; i<myArray.length; i++)=20
=09    myArray [i] =3D Verify.random(10);

=09int max =3D findMax (myArray);
=09for (int i=3D0; i<myArray.length; i++)=20
=09    assert (max >=3D myArray[i]);
    }
}

This can be compiled with javac by having gov.nasa.jpf.jvm.Verify in
classpath. Run jpf on the class file. The error trace has Random#i at
different points which collectively comprise the counterexample.
Perhaps, at present there is no easier way of looking at the
assignment of the variables in the form of a "watch window" of a
standard debugger.

/Ali
--=20
IMP Student
Dependable Computer Systems
Chalmers University of Technology, Sweden


On 7/19/05, Muhammad Ali Shah <muh...@gm...> wrote:
> Hi,
>=20
> Is it possible to verify methods without any invokation code? For
> example, consider the following class:
>=20
> public class Main {
>     public int findMax (int []a) {
>         int k =3D 1;
>         int max =3D a[1];
>=20
>         while (k < a.length) {
>             if (a[k] > max) max =3D a[k];
>             k++;
>         }
>=20
>         return max;
>     }
>=20
>     public static void main (String args[]) {
>     }
> }
>=20
>=20
> The method findMax will throw exception if invoked with an array of
> size 1. Also, it fails to find the maximum element when the max
> element is at index 0 (but for that we would be required to specify
> the property in some way).
>=20
> Is it possible to check the index out of bound issue with JPF? Any
> hints will be highly appreciated.
>=20
> /Ali
>

[Javapathfinder-user] JPF for Methods?

[Muhammad A. S. <muh...@gm...>]

Hi,

Is it possible to verify methods without any invokation code? For
example, consider the following class:

public class Main {
    public int findMax (int []a) {
=09int k =3D 1;
=09int max =3D a[1];

=09while (k < a.length) {
=09    if (a[k] > max) max =3D a[k];
=09    k++;
=09}

=09return max;
    }

    public static void main (String args[]) {
    }
}


The method findMax will throw exception if invoked with an array of
size 1. Also, it fails to find the maximum element when the max
element is at index 0 (but for that we would be required to specify
the property in some way).

Is it possible to check the index out of bound issue with JPF? Any
hints will be highly appreciated.

/Ali

[Javapathfinder-user] Generating counter examples

[Muhammad A. S. <muh...@gm...>]

Hi!

I'm interested in usping JPF for generating counter examples. I've
read a paper titled "Test Input Generation with Java Pathfinder" but
my limited knowledge of JPF itself is a hinderance towards using it
for my purpose.

Can somebody guide me what I should be reading for generating
counterexamples? An interesting example of what I want to do can be:

The following code swaps two positions in an integer array.

a[i] +=3D a[j];
a[j] =3D a[i] - a[j];
a[i] -=3D a[j];

However, it fails to swap the positions when i and j both point to the
same element, i.e., i =3D j (of course there are other problems like
array index out of bound, etc. but that can be handled by pre
conditions).

Any help will be highly appreciated.

/Ali
--
IMP Student
Dependable Computer Systems
Chalmers University of Technology, Sweden

Re: [Javapathfinder-user] I can't execute JPF

[Peter C. M. <pcm...@em...>]

that is the Java 1.5/BCEL issue mentioned in some of the forum/bug 
messages a while ago - the official BCEL 5.1 release is not Java 1.5 
compatible. If you use the bcel CVS version (or the lib that is 
provided with JPF), this should not happen, but there are still some 
other Java 1.5 issues left. Consider Java 1.5 to be not supported for 
now (this will be resolved soon, with the advent of Java 1.5 on OS X)

-- Peter


On Jul 13, 2005, at 12:45 AM, Taehoon, Lee wrote:

>
> I'can't execute JPF
> why I can't execute JPF ??
>
>
> ~/sw/javapathfinder/examples$ java gov.nasa.jpf.JPF Helloworld
> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames
> Research Center
> java.lang.RuntimeException: Unknown or invalid constant type at 364
> at org.apache.bcel.generic.LDC.getType(LDC.java:148)
> at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:47)
> at gov.nasa.jpf.jvm.bytecode.Instruction.init(Instruction.java:194)
> at gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:145)
> at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:623)
> at gov.nasa.jpf.jvm.MethodInfo.<init>(MethodInfo.java:183)
> at gov.nasa.jpf.jvm.MethodInfo.newInstance(MethodInfo.java:257)
> at gov.nasa.jpf.jvm.ClassInfo.loadMethods(ClassInfo.java:1167)
> at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
> at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:349)
> at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1269)
> at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:279)
> at gov.nasa.jpf.JPF.run(JPF.java:248)
> at gov.nasa.jpf.JPF.main(JPF.java:198)
> java.lang.StringIndexOutOfBoundsException: String index out of range: 
> -3
> at java.lang.String.substring(String.java:1768)
> at java.lang.String.substring(String.java:1735)
> at gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:155)
> at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:623)
> at gov.nasa.jpf.jvm.MethodInfo.<init>(MethodInfo.java:183)
> at gov.nasa.jpf.jvm.MethodInfo.newInstance(MethodInfo.java:257)
> at gov.nasa.jpf.jvm.ClassInfo.loadMethods(ClassInfo.java:1167)
> at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
> at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:349)
> at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1269)
> at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:279)
> at gov.nasa.jpf.JPF.run(JPF.java:248)
> at gov.nasa.jpf.JPF.main(JPF.java:198)
>
>
> -------------------------------------------------------
> This SF.Net email is sponsored by the 'Do More With Dual!' webinar 
> happening
> July 14 at 8am PDT/11am EDT. We invite you to explore the latest in 
> dual
> core and dual graphics technology at this free one hour event hosted 
> by HP,
> AMD, and NVIDIA.  To register visit http://www.hp.com/go/dualwebinar
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

[Javapathfinder-user] I can't execute JPF

[Taehoon, L. <ta...@ky...>]

I'can't execute JPF
why I can't execute JPF ??


~/sw/javapathfinder/examples$ java gov.nasa.jpf.JPF Helloworld
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA Ames
Research Center
java.lang.RuntimeException: Unknown or invalid constant type at 364
at org.apache.bcel.generic.LDC.getType(LDC.java:148)
at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:47)
at gov.nasa.jpf.jvm.bytecode.Instruction.init(Instruction.java:194)
at gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:145)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:623)
at gov.nasa.jpf.jvm.MethodInfo.<init>(MethodInfo.java:183)
at gov.nasa.jpf.jvm.MethodInfo.newInstance(MethodInfo.java:257)
at gov.nasa.jpf.jvm.ClassInfo.loadMethods(ClassInfo.java:1167)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:349)
at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1269)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:279)
at gov.nasa.jpf.JPF.run(JPF.java:248)
at gov.nasa.jpf.JPF.main(JPF.java:198)
java.lang.StringIndexOutOfBoundsException: String index out of range: -3
at java.lang.String.substring(String.java:1768)
at java.lang.String.substring(String.java:1735)
at gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:155)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:623)
at gov.nasa.jpf.jvm.MethodInfo.<init>(MethodInfo.java:183)
at gov.nasa.jpf.jvm.MethodInfo.newInstance(MethodInfo.java:257)
at gov.nasa.jpf.jvm.ClassInfo.loadMethods(ClassInfo.java:1167)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:349)
at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1269)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:279)
at gov.nasa.jpf.JPF.run(JPF.java:248)
at gov.nasa.jpf.JPF.main(JPF.java:198)

Re: [Javapathfinder-user] Specifying properties using 'Listener' scheme

[Peter C. M. <pcm...@em...>]

Sorry for not responding earlier, it's proposal season and everybody is=20=

a bit busy.

There are two ways to implement properties, both described in the docu=20=

under "how to implement properties": gov.nasa.jpf.Property and=20
VM/SearchListener.

As a rule of thumb, I would say the older 'Property' is more for simple=20=

conditions where you just have to query some existing (more complex)=20
state of the VM or the Search to find out if the property holds (like=20
NoUncaughtExceptionsProperty, NotDeadlockedProperty etc.). The=20
Listeners are more versatile, but naturally you have to do more. There=20=

is a mistake in the docu, which says that you can use=20
Search.terminate() to indicate failure, but I somehow went with the=20
scheme of implementing the Property interface in the Listener, then=20
just query the internal Listener state in the Property.check() (no=20
changes to Search classes required that way). Look at=20
gov.nasa.jpf.tools.HeapTracker as an example. If you are in doubt=20
because your property looks complicated, I would say this is almost=20
certainly the right way to go - there are no limits what you can do=20
here.

Safety property, that is. One thing I had in mind for a while was using=20=

DynamicAssertions to do temporal stuff (i.e. turn part of the property=20=

into an JPF object, and use something like AspectJ to do the=20
instrumentation), but there's no example for this yet. The other way to=20=

do temporal logic by means of the LTL2Buchi extension is not functional=20=

anymore - Dimitra's translator works fine, but the LTLSearch is=20
certainly defunct (until somebody fixes it, hint, hint).

hope this helps a bit
-- Peter

On Jul 7, 2005, at 6:55 PM, M=EDrian Bruckschen wrote:

> Hi all,
>
> We're an undergraduate group of students and we're trying to verify
> some properties in a work a friend of us has done, that is an
> object-oriented DMBS.
>
> We have simplified the most we could the code, and we started by
> verifying the DBMS server. Or tried to.
>
> We've read the documentation available at the site, and have chosen to
> verify using listeners (cause we need to step by the states generated,
> and it seemed to us the best way to do it). But we are not really
> confident of how to specify the properties. Is there any simpler
> documentation on it? Can anybody point us the right way to go? How can
> we specify properties for JPF to verify using listeners?
>
> Thanks for your attention,

[Javapathfinder-user] Specifying properties using 'Listener' scheme

[<cl...@gm...>]

Hi all,

We're an undergraduate group of students and we're trying to verify
some properties in a work a friend of us has done, that is an
object-oriented DMBS.

We have simplified the most we could the code, and we started by
verifying the DBMS server. Or tried to.

We've read the documentation available at the site, and have chosen to
verify using listeners (cause we need to step by the states generated,
and it seemed to us the best way to do it). But we are not really
confident of how to specify the properties. Is there any simpler
documentation on it? Can anybody point us the right way to go? How can
we specify properties for JPF to verify using listeners?

Thanks for your attention,

--=20
M=EDrian Bruckschen

Re: [Javapathfinder-user] Verify.randomDouble

[Peter C. M. <pcm...@em...>]

Work in progress (actually I just got back to this topic). The idea is 
that we want to associate choice generator objects with each state that 
has nondeterministic choices, i.e. delegate the enumeration of choice 
values to dedicated objects. This would allow more than just the simple 
integer interval that's currently kind of hard-wired into the Scheduler 
(where it doesn't really belong). My favorite example for this are 
random floating point values - quite obvious there is no complete 
enumeration, but there are plenty of potential (application specific) 
heuristics (e.g. a "threshold value" choice generator).

The Verify.randomDouble() is not functional yet, and the interface will 
change.

-- Peter

On Jun 10, 2005, at 7:20 AM, Ladislav Prosek wrote:
> could anyone please explain what is the exact semantics of the 
> Verify.randomDouble(String) method? The stub in Verify.java is not 
> commented.

[Javapathfinder-user] Verify.randomDouble

[Ladislav P. <lad...@ma...>]

Hi,

could anyone please explain what is the exact semantics of the 
Verify.randomDouble(String) method? The stub in Verify.java is not 
commented.

Thanks!
LP 

Re: [Javapathfinder-user] Class.newInstance() not yet supported

[Peter C. M. <pcm...@em...>]

sorry for not responding earlier, but I thought I implement the thing 
first :)

Well, it's not completely implemented (the exceptions are still 
missing), but the real challenge was somewhere else - reflective 
functions (incl object creation) have to be done from a native method 
(a NativePeer - see MJI docu) so that we can get to the JPF innards 
(type info, heap allocation etc.). The problem is that this includes 
some round trip where we start in JPF executed code, from there call a 
native method that is executed in the host VM, from there execute some 
bytecode back in JPF (in the case of Class.newInstance(), this is the 
default ctor).

It's a tricky problem, and there are still some serious caveats (you 
are not allowed to block from the JPF executed code you call back 
into), but the important infrastructure is in place.

As to your question - Class.newInstance() should work now (less 
exceptions), but that's pretty much the frontier for reflection for 
now.

-- Peter 


On May 3, 2005, at 2:39 PM, Atwood, John Wesley wrote:
> JPF users,
>
> Trying to learn about JPF, I ran the jpf run-tests, and a few of the
> examples.
> Then I ran it on my own program, and get:
> 	Class.newInstance() not yet supported
>
> Is all dynamic object creation prohibited, and, if so, is that a
> fundamental aspect of JPF?
>
> Thanks,
>
> John Atwood

Re: [Javapathfinder-user] Class.newInstance() not yet supported

[John P. <joh...@na...>]

Hi John,

sorry i wasn't clear.

I meant that "new" works now:

  String x = new String("bob");

will allocate a String object on the heap.


Class.getInstance() does not work - someones need to implement it so it 
pokes into the JPF JVM and do what new does.  we have not done that - 
apparently we have only used new to allocateo on the heap.


jp




Atwood, John Wesley wrote:
> Jp,
> 
> I don't quite follow "new should work just fine".  Do you mean "should,
> with add'l development", or "should...must be a bug"?
> 
> I read in the source, that newInstance is "required by some braindead
> IDE's..."; but the line that generates this seems fairly innocuous to
> me:
> 	String url = "blah";
> 
> I'll look in the papers for more background....
> 
> John
> -----Original Message-----
> From: John Penix [mailto:joh...@na...] 
> Sent: Tuesday, May 03, 2005 3:07 PM
> To: Atwood, John Wesley
> Cc: jav...@li...
> Subject: Re: [Javapathfinder-user] Class.newInstance() not yet supported
> 
> Hi John,
> 
> new should work just fine.
> 
> this is an example of a Javaism that we have not been using in our
> "models" of NASA applications.
> 
> The code which models java/lang/Class is in
> /env/jpf/java/lang/Class.java - the 'real' class has native methods, so
> we have to model it.  The methods in java/lang/Class are only minimally
> supported - just enough to support assertions.  (see the comments at the
> top)
> 
> 
> supporting newInstance seems like a big deal to me.  I don't know how
> hard it would be to hook that in - Peter or Willem should be able to
> guess.
> 
> If anyone is feeling slightly ambitious, grab the MJI docs and go for
> it. :)
> 
> 
> jp
> 
> 
> Atwood, John Wesley wrote:
> 
>>JPF users,
>>
>>Trying to learn about JPF, I ran the jpf run-tests, and a few of the 
>>examples.
>>Then I ran it on my own program, and get:
>>	Class.newInstance() not yet supported
>>
>>Is all dynamic object creation prohibited, and, if so, is that a 
>>fundamental aspect of JPF?
>>
>>Thanks,
>>
>>
>>John Atwood
>>
>>
>>-------------------------------------------------------
>>This SF.Net email is sponsored by: NEC IT Guy Games.
>>Get your fingers limbered up and give it your best shot. 4 great 
>>events, 4 opportunities to win big! Highest score wins.NEC IT Guy 
>>Games. Play to win an NEC 61 plasma display. Visit 
>>http://www.necitguy.com/?r 
>>_______________________________________________
>>Javapathfinder-user mailing list
>>Jav...@li...
>>https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>>
> 
> 
> --
> John Penix PhD. john.penix+nasa.gov http://ase.arc.nasa.gov/jpenix/
> Robust Software Engineering Group  ph:(650)604-6576 bld:N296 rm:268
> Intelligent Systems Division  NASA Ames Research Center  Mt.View CA
> 
> 
> 
> 
> 
> -------------------------------------------------------
> This SF.Net email is sponsored by: NEC IT Guy Games.
> Get your fingers limbered up and give it your best shot. 4 great events, 4
> opportunities to win big! Highest score wins.NEC IT Guy Games. Play to
> win an NEC 61 plasma display. Visit http://www.necitguy.com/?r 
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
> 

-- 
John Penix PhD. john.penix+nasa.gov http://ase.arc.nasa.gov/jpenix/
Robust Software Engineering Group  ph:(650)604-6576 bld:N296 rm:268
Intelligent Systems Division  NASA Ames Research Center  Mt.View CA

RE: [Javapathfinder-user] Class.newInstance() not yet supported

[Atwood, J. W. <joh...@hp...>]

Jp,

I don't quite follow "new should work just fine".  Do you mean "should,
with add'l development", or "should...must be a bug"?

I read in the source, that newInstance is "required by some braindead
IDE's..."; but the line that generates this seems fairly innocuous to
me:
	String url =3D "blah";

I'll look in the papers for more background....

John
-----Original Message-----
From: John Penix [mailto:joh...@na...]=20
Sent: Tuesday, May 03, 2005 3:07 PM
To: Atwood, John Wesley
Cc: jav...@li...
Subject: Re: [Javapathfinder-user] Class.newInstance() not yet supported

Hi John,

new should work just fine.

this is an example of a Javaism that we have not been using in our
"models" of NASA applications.

The code which models java/lang/Class is in
/env/jpf/java/lang/Class.java - the 'real' class has native methods, so
we have to model it.  The methods in java/lang/Class are only minimally
supported - just enough to support assertions.  (see the comments at the
top)


supporting newInstance seems like a big deal to me.  I don't know how
hard it would be to hook that in - Peter or Willem should be able to
guess.

If anyone is feeling slightly ambitious, grab the MJI docs and go for
it. :)


jp


Atwood, John Wesley wrote:
> JPF users,
>=20
> Trying to learn about JPF, I ran the jpf run-tests, and a few of the=20
> examples.
> Then I ran it on my own program, and get:
> 	Class.newInstance() not yet supported
>=20
> Is all dynamic object creation prohibited, and, if so, is that a=20
> fundamental aspect of JPF?
>=20
> Thanks,
>=20
>=20
> John Atwood
>=20
>=20
> -------------------------------------------------------
> This SF.Net email is sponsored by: NEC IT Guy Games.
> Get your fingers limbered up and give it your best shot. 4 great=20
> events, 4 opportunities to win big! Highest score wins.NEC IT Guy=20
> Games. Play to win an NEC 61 plasma display. Visit=20
> http://www.necitguy.com/?r=20
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>=20

--
John Penix PhD. john.penix+nasa.gov http://ase.arc.nasa.gov/jpenix/
Robust Software Engineering Group  ph:(650)604-6576 bld:N296 rm:268
Intelligent Systems Division  NASA Ames Research Center  Mt.View CA

Re: [Javapathfinder-user] Class.newInstance() not yet supported

[John P. <joh...@na...>]

Hi John,

new should work just fine.

this is an example of a Javaism that we have not been using in our 
"models" of NASA applications.

The code which models java/lang/Class is in 
/env/jpf/java/lang/Class.java - the 'real' class has native methods, so 
we have to model it.  The methods in java/lang/Class are only minimally 
supported - just enough to support assertions.  (see the comments at the 
top)


supporting newInstance seems like a big deal to me.  I don't know how 
hard it would be to hook that in - Peter or Willem should be able to guess.

If anyone is feeling slightly ambitious, grab the MJI docs and go for it. :)


jp


Atwood, John Wesley wrote:
> JPF users,
> 
> Trying to learn about JPF, I ran the jpf run-tests, and a few of the
> examples.
> Then I ran it on my own program, and get:
> 	Class.newInstance() not yet supported
> 
> Is all dynamic object creation prohibited, and, if so, is that a
> fundamental aspect of JPF?
> 
> Thanks,
> 
> 
> John Atwood
> 
> 
> -------------------------------------------------------
> This SF.Net email is sponsored by: NEC IT Guy Games.
> Get your fingers limbered up and give it your best shot. 4 great events, 4
> opportunities to win big! Highest score wins.NEC IT Guy Games. Play to
> win an NEC 61 plasma display. Visit http://www.necitguy.com/?r 
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
> 

-- 
John Penix PhD. john.penix+nasa.gov http://ase.arc.nasa.gov/jpenix/
Robust Software Engineering Group  ph:(650)604-6576 bld:N296 rm:268
Intelligent Systems Division  NASA Ames Research Center  Mt.View CA

[Javapathfinder-user] Class.newInstance() not yet supported

[Atwood, J. W. <joh...@hp...>]

JPF users,

Trying to learn about JPF, I ran the jpf run-tests, and a few of the
examples.
Then I ran it on my own program, and get:
	Class.newInstance() not yet supported

Is all dynamic object creation prohibited, and, if so, is that a
fundamental aspect of JPF?

Thanks,


John Atwood

[Javapathfinder-user] convenience libs upload

[Peter C. M. <pcm...@em...>]

I just uploaded two separate zip archives

- jpf-lib.zip
- jpf-build-tools.zip

containing 3rd party runtime and build libraries for
JavaPathFinder. See the "Prerequisites" doc for details.

Unzip both in the JavaPathFinder root dir. Contents should be
automatically picked up if you use

bin/jpf - to start JavaPathFinder
build-tools/bin/ant - to build the system

No need for any additional CLASSPATH settings.

Both archives are strictly for your convenience, and not
required if you already have installed these libs (e.g. as part
of Eclipse)

-- Peter

[Javapathfinder-user] welcome

[Peter C. M. <pcm...@em...>]

Welcome - this is the inaugural message for the user list

-- Peter