Menu
▾
▴
javapathfinder-user — usage related topics (installing, running, options, output...)
You can subscribe to this list here.
| 2005 |
Jan
|
Feb
|
Mar
|
Apr
(3) |
May
(5) |
Jun
(2) |
Jul
(9) |
Aug
(7) |
Sep
(4) |
Oct
(7) |
Nov
(20) |
Dec
(5) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2006 |
Jan
(1) |
Feb
(8) |
Mar
(17) |
Apr
(25) |
May
(7) |
Jun
(1) |
Jul
|
Aug
(1) |
Sep
(14) |
Oct
(5) |
Nov
(1) |
Dec
(5) |
| 2007 |
Jan
(7) |
Feb
(3) |
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
(4) |
Sep
(8) |
Oct
(7) |
Nov
(2) |
Dec
(11) |
| 2008 |
Jan
(1) |
Feb
(9) |
Mar
(3) |
Apr
(8) |
May
(2) |
Jun
(6) |
Jul
(5) |
Aug
(13) |
Sep
(2) |
Oct
(7) |
Nov
(3) |
Dec
(28) |
| 2009 |
Jan
(10) |
Feb
(19) |
Mar
(12) |
Apr
(10) |
May
|
Jun
(1) |
Jul
|
Aug
(1) |
Sep
(2) |
Oct
(3) |
Nov
|
Dec
|
| 2010 |
Jan
(1) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2015 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
|
Dec
|
|
From: Markeloff, R. <Ric...@sp...> - 2006-09-01 16:42:37
|
I successfully installed the svn client, retrieved the files from the repository, and created an Eclipse project. However, I've encountered the following problems: =20 1) Numerous build errors in examples/issta2006 and test/gov/nasa/jpf/peterd_tests. I just deleted these packages from the project. =20 2) When I attempt to run the Deadlock example, I get the following: =20 JPF configuration error: class not found gov.nasa.jpf.filter.FilteringSerializer > used within "vm.class" instantiation of class gov.nasa.jpf.jvm.JVM =20 I don't see any gov.nasa.jpf.filter package in the distribution. Where could it be? =20 Thanks, =20 Rich Markeloff =20 |
|
From: Yulia A. <ts...@ja...> - 2006-08-31 15:19:55
|
Hi =20 All you u r PHAR c RM y ACY dir j ec r tly from the man f uf a actur k er, Your ch o an f ce to e y cono f mize wit o h us http://lakionmertinher.com d=20 j=20 b=20 ones. Until we found out we had to act as though there were. I kept How long? I would. I want you two just where you are. |
|
From: Markeloff, R. <Ric...@sp...> - 2006-06-16 16:06:05
|
I'd like to use JPF to check an application that makes extensive use of the classes in java.nio.channels. I'd like to use MJI to move this part of the code from the JPF VM to the underlying VM. Has anyone done this before? I'd be interested in hearing from anyone who has gone down this road before. Thanks, Rich Markeloff =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 =20 Richard Markeloff SPARTA, Inc. 1911 N. Fort Myer Dr., Suite 1100 Arlington, VA 22209 =20 Voice: 703 647 2414 Fax: 703 558 3410 |
|
From: John P. <jp...@go...> - 2006-05-23 05:46:56
|
Hi Sergey, Someone recently posted a message about trying to find a known deadlock in the StringBuffer inplementation. They may have even posted the result. I've look into using JPF with JUnit - JUnit will pick up all methods named testXXX from classes derived from junit.TestCase and run them. JPF doesn't support the Java reflection features required to ru nthe JUnit framework classes. John On 5/22/06, Sergey Kulikov <se...@cs...> wrote: > Thanks for your reply Willem, > > what about other classes? Say LinkedList... to test for deadlocks and > uncaught exceptions. > > I understand that it is not hard to manually write a main method to test > a particular class. However that would be tedious to test all of the > classes since JPF needs a main method for each of the class. > > Has any work been done in automatically generating a main method? > > thanks > sergey > > > On Mon, 22 May 2006, Willem Visser wrote: > > > Hi Sergey, > > > > It has not yet been used to analyze the concurrency classes. This would > > be very interesting I think. As for other big projects the two biggest > > I'm aware of are a +-7KLOC rover executive here at Ames and a (much > > bigger) enterprise software package from Fujitsu (described in a SoftMc > > 2005 paper). > > > > Bye, > > Willem > > > > -- > > Willem C. Visser Automated Software Engineering Group > > RIACS/NASA Ames Research Center wv...@em... > > M/S 269-2 http://ase.arc.nasa.gov > > Moffett Field, CA 94035 (650)604-3515 fax 4036 rm 235 > > > > > >> -----Original Message----- > >> From: jav...@li... > >> [mailto:jav...@li...] On Behalf Of > >> Sergey Kulikov > >> Sent: Wednesday, May 17, 2006 8:22 AM > >> To: jav...@li... > >> Subject: [Javapathfinder-user] what has JPF been used on? > >> > >> > >> Has JPF been ever used on detecting concurrency related bugs > > (deadlocks, > >> race conditions) in the Java standard library classes? I'm refering to > >> those classes that support concurrency. > >> > >> What other big projects (apart from those at NASA) has JPF been used > > on. > >> Any info/links would be appreciated. > >> > >> thanks > >> sergey > >> > >> > >> ------------------------------------------------------- > >> Using Tomcat but need to do more? Need to support web services, > > security? > >> Get stuff done quickly with pre-integrated technology to make your job > >> easier > >> Download IBM WebSphere Application Server v.1.0.1 based on Apache > > Geronimo > >> > > http://sel.as-us.falkag.net/sel?cmd=3Dlnk&kid=3D120709&bid=3D263057&dat= =3D121642 > >> _______________________________________________ > >> Javapathfinder-user mailing list > >> Jav...@li... > >> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > > > > > > > ------------------------------------------------------- > Using Tomcat but need to do more? Need to support web services, security? > Get stuff done quickly with pre-integrated technology to make your job ea= sier > Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronim= o > http://sel.as-us.falkag.net/sel?cmd=3Dlnk&kid=3D120709&bid=3D263057&dat= =3D121642 > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > |
|
From: Sergey K. <se...@cs...> - 2006-05-23 03:27:16
|
Thanks for your reply Willem, what about other classes? Say LinkedList... to test for deadlocks and uncaught exceptions. I understand that it is not hard to manually write a main method to test a particular class. However that would be tedious to test all of the classes since JPF needs a main method for each of the class. Has any work been done in automatically generating a main method? thanks sergey On Mon, 22 May 2006, Willem Visser wrote: > Hi Sergey, > > It has not yet been used to analyze the concurrency classes. This would > be very interesting I think. As for other big projects the two biggest > I'm aware of are a +-7KLOC rover executive here at Ames and a (much > bigger) enterprise software package from Fujitsu (described in a SoftMc > 2005 paper). > > Bye, > Willem > > -- > Willem C. Visser Automated Software Engineering Group > RIACS/NASA Ames Research Center wv...@em... > M/S 269-2 http://ase.arc.nasa.gov > Moffett Field, CA 94035 (650)604-3515 fax 4036 rm 235 > > >> -----Original Message----- >> From: jav...@li... >> [mailto:jav...@li...] On Behalf Of >> Sergey Kulikov >> Sent: Wednesday, May 17, 2006 8:22 AM >> To: jav...@li... >> Subject: [Javapathfinder-user] what has JPF been used on? >> >> >> Has JPF been ever used on detecting concurrency related bugs > (deadlocks, >> race conditions) in the Java standard library classes? I'm refering to >> those classes that support concurrency. >> >> What other big projects (apart from those at NASA) has JPF been used > on. >> Any info/links would be appreciated. >> >> thanks >> sergey >> >> >> ------------------------------------------------------- >> Using Tomcat but need to do more? Need to support web services, > security? >> Get stuff done quickly with pre-integrated technology to make your job >> easier >> Download IBM WebSphere Application Server v.1.0.1 based on Apache > Geronimo >> > http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 >> _______________________________________________ >> Javapathfinder-user mailing list >> Jav...@li... >> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > > |
|
From: Willem V. <wv...@em...> - 2006-05-22 17:46:16
|
Hi Sergey, It has not yet been used to analyze the concurrency classes. This would be very interesting I think. As for other big projects the two biggest I'm aware of are a +-7KLOC rover executive here at Ames and a (much bigger) enterprise software package from Fujitsu (described in a SoftMc 2005 paper). Bye, Willem -- Willem C. Visser Automated Software Engineering Group RIACS/NASA Ames Research Center wv...@em... M/S 269-2 http://ase.arc.nasa.gov Moffett Field, CA 94035 (650)604-3515 fax 4036 rm 235 > -----Original Message----- > From: jav...@li... > [mailto:jav...@li...] On Behalf Of > Sergey Kulikov > Sent: Wednesday, May 17, 2006 8:22 AM > To: jav...@li... > Subject: [Javapathfinder-user] what has JPF been used on? > > > Has JPF been ever used on detecting concurrency related bugs (deadlocks, > race conditions) in the Java standard library classes? I'm refering to > those classes that support concurrency. > > What other big projects (apart from those at NASA) has JPF been used on. > Any info/links would be appreciated. > > thanks > sergey > > > ------------------------------------------------------- > Using Tomcat but need to do more? Need to support web services, security? > Get stuff done quickly with pre-integrated technology to make your job > easier > Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo > http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user |
|
From: Sergey K. <se...@cs...> - 2006-05-17 15:21:47
|
Has JPF been ever used on detecting concurrency related bugs (deadlocks, race conditions) in the Java standard library classes? I'm refering to those classes that support concurrency. What other big projects (apart from those at NASA) has JPF been used on. Any info/links would be appreciated. thanks sergey |
|
From: Jenny c. <je...@gm...> - 2006-05-15 08:38:58
|
Hi,
I'm having trouble with the ArrayIndexOutOfBoundsException. I'm not sure if
it's a problem of my application or not. Did anyone have this problem
before?
Thanks,
Jenny
Java Pathfinder Model Checker v3.1.2 - (C) 1999-2005 RIACS/NASA Ames
Research Center
JPF exception, terminating: class java.lang.ArrayIndexOutOfBoundsException:
9
java.lang.ArrayIndexOutOfBoundsException: 9
at gov.nasa.jpf.jvm.StackFrame.push(StackFrame.java:862)
at gov.nasa.jpf.jvm.ThreadInfo.push(ThreadInfo.java:1853)
at gov.nasa.jpf.jvm.ThreadInfo.finish(ThreadInfo.java:1584)
at gov.nasa.jpf.jvm.ThreadInfo.popFrame(ThreadInfo.java:1808)
at gov.nasa.jpf.jvm.ThreadInfo.throwException(ThreadInfo.java:1961)
at gov.nasa.jpf.jvm.bytecode.ATHROW.execute(ATHROW.java:43)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1508)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2104)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1568)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1120)
at gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)
at gov.nasa.jpf.JPF.run(JPF.java:311)
at gov.nasa.jpf.JPF.main(JPF.java:238)
java.lang.ArrayIndexOutOfBoundsException: 9
at gov.nasa.jpf.jvm.StackFrame.push(StackFrame.java:862)
at gov.nasa.jpf.jvm.ThreadInfo.push(ThreadInfo.java:1853)
at gov.nasa.jpf.jvm.ThreadInfo.finish(ThreadInfo.java:1584)
at gov.nasa.jpf.jvm.ThreadInfo.popFrame(ThreadInfo.java:1808)
at gov.nasa.jpf.jvm.ThreadInfo.throwException(ThreadInfo.java:1961)
at gov.nasa.jpf.jvm.bytecode.ATHROW.execute(ATHROW.java:43)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1508)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2104)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1568)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1120)
at gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)
at gov.nasa.jpf.JPF.run(JPF.java:311)
at gov.nasa.jpf.JPF.main(JPF.java:238)
gov.nasa.jpf.JPFException: class java.lang.ArrayIndexOutOfBoundsException: =
9
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1163)
at gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)
at gov.nasa.jpf.JPF.run(JPF.java:311)
at gov.nasa.jpf.JPF.main(JPF.java:238)
|
|
From: John P. <jp...@go...> - 2006-05-02 16:51:23
|
Hi Jenny, I think you are having one of the two following problems: make sure you have JPF's vm.bootclasspath configured to point to where the ../javapathfinder/env/jpf/.. .class files are being put - if you are using ant with build.xml it should be javapathfinder/build/env/jpf/ but if you ar= e building with Eclipse you need to either tell it to put them there, or poin= t JPF at them. also, make sure you are using the version of BCEL we distribute with JPF - we have fixed a few BCEL issues in our version. John On 5/2/06, Jenny choe <je...@gm...> wrote: > > Hi, > > I'm having trouble running JPF with example class files in eclipse. I set > the project to point the "jpf release" directory, used gov.nasa.jpf.JPF a= s > main class and set Bakery_original as a program argument. > > I've got this error message below: > error during VM runtime initialization: > uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError: > java.lang.Object.registerNatives (no peer) > at java.lang.Object.<clinit>(java\lang\Object.java:24) > > Have anyone seen this before? > > Thanks, > Jenny > > |
|
From: Jenny c. <je...@gm...> - 2006-05-02 07:08:43
|
Hi,
I'm having trouble running JPF with example class files in eclipse. I set
the project to point the "jpf release" directory, used gov.nasa.jpf.JPF as
main class and set Bakery_original as a program argument.
I've got this error message below:
error during VM runtime initialization:
uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError:
java.lang.Object.registerNatives (no peer)
at java.lang.Object.<clinit>(java\lang\Object.java:24)
Have anyone seen this before?
Thanks,
Jenny
|
|
From: Willem V. <wv...@em...> - 2006-04-21 21:05:24
|
Hi Richard, TestJPF is not really a test so it is fine that it fails. It is just a naming convention problem: everything starting with Test. is considered a test for junit, but this one is not a real test it is just our code for running jpf during junit tests. Bye, Willem -- Willem C. Visser Automated Software Engineering Group RIACS/NASA Ames Research Center wv...@em... M/S 269-2 http://ase.arc.nasa.gov Moffett Field, CA 94035 (650)604-3515 fax 4036 rm 235 -----Original Message----- From: jav...@li... [mailto:jav...@li...] On Behalf Of Markeloff, Richard Sent: Friday, April 21, 2006 5:21 AM To: jav...@li... Subject: [Javapathfinder-user] TestJPF fails When I do ant run-tests, there are no compile errors and all tests pass except TestJPF. Does this indicate a problem with my set up? I am using the latest code from CVS, the jars and ant downloaded from sourceforge.net, and Java 1.4.2_04. Thank you, Rich Markeloff ________________________________ Richard Markeloff SPARTA, Inc. 1911 N. Fort Myer Dr., Suite 1100 Arlington, VA 22209 Voice: 703 647 2414 Fax: 703 558 3410 |
|
From: Markeloff, R. <Ric...@sp...> - 2006-04-21 12:20:43
|
When I do ant run-tests, there are no compile errors and all tests pass except TestJPF. Does this indicate a problem with my set up? =20 I am using the latest code from CVS, the jars and ant downloaded from sourceforge.net, and Java 1.4.2_04. =20 Thank you, =20 Rich Markeloff =20 ________________________________ =20 Richard Markeloff SPARTA, Inc. 1911 N. Fort Myer Dr., Suite 1100 Arlington, VA 22209 =20 Voice: 703 647 2414 Fax: 703 558 3410 =20 |
|
From: John P. <jp...@go...> - 2006-04-17 18:33:50
|
Hi Richard,
what compiler version are you running?
John
On 4/17/06, Markeloff, Richard <Ric...@sp...> wrote:
>
> I had no trouble checking out JPF from CVS, but when I attempt to do ant
> run-tests I get the following error:
>
>
>
> [javac]
> /home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/SimpleIdleFi=
lter.java:36:
> error: Class or interface `java.util.logging.Logger' not found in import.
>
> [javac] import java.util.logging.Logger;
>
> [javac] ^
>
> [javac]
> /home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/SimpleIdleFi=
lter.java:48:
> error: Type `Logger' not found in declaration of field `log'.
>
> [javac] static Logger log =3D JPF.getLogger("
> gov.nasa.jpf.tools.SimpleIdleFilter");
>
> [javac] ^
>
> [javac]
> /home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.j=
ava:36:
> error: Class or interface `java.util.logging.Logger' not found in import.
>
> [javac] import java.util.logging.Logger;
>
> [javac] ^
>
> [javac]
> /home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.j=
ava:58:
> error: Type `Logger' not found in declaration of field `log'.
>
> [javac] static Logger log =3D JPF.getLogger("
> gov.nasa.jpf.tools.IdleFilter");
>
> [javac] ^
>
> [javac]
> /home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/search/AbstractSea=
rch.java:0:
> internal compiler error: Segmentation fault
>
> [javac] Please submit a full bug report,
>
> [javac] with preprocessed source if appropriate.
>
> [javac] See <URL:http://bugzilla.redhat.com/bugzilla/<http://www.goog=
le.com/url?sa=3DD&q=3Dhttp%3A%2F%2Fbugzilla.redhat.com%2Fbugzilla%2F>>
> for instructions.
>
>
>
> I have never encountered an error like this before. Is there really
> something wrong with my java compiler, or is this perhaps caused by
> something in build.xml?
>
>
>
> Thank you,
>
>
>
> Rich Markeloff
>
>
>
> *________________________________*
>
>
>
> Richard Markeloff
>
> SPARTA, Inc.
>
> 1911 N. Fort Myer Dr., Suite 1100
>
> Arlington, VA 22209
>
>
>
> Voice: 703 647 2414
>
> Fax: 703 558 3410
>
>
>
|
|
From: Markeloff, R. <Ric...@sp...> - 2006-04-17 18:10:29
|
I had no trouble checking out JPF from CVS, but when I attempt to do ant
run-tests I get the following error:
=20
[javac]
/home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/SimpleIdleF
ilter.java:36: error: Class or interface `java.util.logging.Logger' not
found in import.
[javac] import java.util.logging.Logger;
[javac] ^
[javac]
/home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/SimpleIdleF
ilter.java:48: error: Type `Logger' not found in declaration of field
`log'.
[javac] static Logger log =3D
JPF.getLogger("gov.nasa.jpf.tools.SimpleIdleFilter");
[javac] ^
[javac]
/home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.
java:36: error: Class or interface `java.util.logging.Logger' not found
in import.
[javac] import java.util.logging.Logger;
[javac] ^
[javac]
/home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.
java:58: error: Type `Logger' not found in declaration of field `log'.
[javac] static Logger log =3D
JPF.getLogger("gov.nasa.jpf.tools.IdleFilter");
[javac] ^
[javac]
/home/markelof/cdp2006/javapathfinder/src/gov/nasa/jpf/search/AbstractSe
arch.java:0: internal compiler error: Segmentation fault
[javac] Please submit a full bug report,
[javac] with preprocessed source if appropriate.
[javac] See <URL:http://bugzilla.redhat.com/bugzilla/> for
instructions.
=20
I have never encountered an error like this before. Is there really
something wrong with my java compiler, or is this perhaps caused by
something in build.xml?
=20
Thank you,
=20
Rich Markeloff
=20
________________________________
=20
Richard Markeloff
SPARTA, Inc.
1911 N. Fort Myer Dr., Suite 1100
Arlington, VA 22209
=20
Voice: 703 647 2414
Fax: 703 558 3410
=20
|
|
From: Willem V. <wv...@em...> - 2006-04-12 19:13:24
|
We are just finishing up a new version of JPF (should be done very soon) at which point I'll add the specific kind of abstract state matching described in that paper as well as a much more elaborate scheme as discussed in an upcoming ISSTA paper. ETA is probably sometime next month. In the longer term we'll make it possible to customize state matching through the main system - note that the one used in the mentioned papers are essentially put on top of JPF rather than inside. ETA for this more elaborate scheme is end of summer. -- Willem C. Visser Automated Software Engineering Group RIACS/NASA Ames Research Center wv...@em... M/S 269-2 http://ase.arc.nasa.gov Moffett Field, CA 94035 (650)604-3515 fax 4036 rm 235 > -----Original Message----- > From: jav...@li... > [mailto:jav...@li...] On Behalf Of Adam > Kiezun > Sent: Wednesday, April 12, 2006 12:07 PM > To: jav...@li... > Subject: [Javapathfinder-user] Abstract state matching > > hi, > (I asked this question on the sourceforge forum before but maybe I'll be > more > lucky here) > > Is abstraction-based state matching available in JPF now? > > I mean something a'la "Test Input Generation for Red Black Trees using > Abstraction" Visser et al (ASE'05) > > If yes, how can I use it? If not, do you have estimated timelime for this > feature? > > Thanks > /adam > > > ------------------------------------------------------- > This SF.Net email is sponsored by xPML, a groundbreaking scripting > language > that extends applications into web and mobile media. Attend the live > webcast > and join the prime developer group breaking into this new coding > territory! > http://sel.as-us.falkag.net/sel?cmd=lnk&kid=110944&bid=241720&dat=121642 > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user |
|
From: Adam K. <ak...@cs...> - 2006-04-12 19:06:41
|
hi, (I asked this question on the sourceforge forum before but maybe I'll be more lucky here) Is abstraction-based state matching available in JPF now? I mean something a'la "Test Input Generation for Red Black Trees using Abstraction" Visser et al (ASE'05) If yes, how can I use it? If not, do you have estimated timelime for this feature? Thanks /adam |
|
From: John P. <jp...@go...> - 2006-04-12 18:10:26
|
Shane, if you run with -show, it will list the vm.classpath (and every other confi= g variable) that it is picking up from the chain of config files. the registerNative peer implementation is in env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java make sure env/jvm is built and in your CLASSPATH John On 4/11/06, Shane Davison <sha...@ho...> wrote: > > > I can't seem to get past this error... > > error during VM runtime initialization: > uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError: > java.lang > .Object.registerNatives (no peer) > at java.lang.Object.<clinit>(java\lang\Object.java:24) > > |
|
From: Adam K. <ak...@cs...> - 2006-04-12 16:59:24
|
> So am I missing some class files? > I just re-ran "run-tests" (after removing TestAssert) and > all the tests ran and passed. But still no Object class under > the path you mentioned (but I do have this file: > build/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.class). Shane, that sounds good. Have you tried running the examples yet? Try deadlock.Deadlock for example /adam |
|
From: Shane D. <sha...@ho...> - 2006-04-12 04:48:48
|
Willem/Adam, Thanks again for your help. I know that at least the build dir was getting created when running ant since it wasn't there before but it was after (and I believe I saw a bunch of classes in there at one point). Here at work (Solaris), I have... a build/env/jvm/gov/nasa/jpf/jvm dir with 22 JPF_java_*.class files nothing in build/test And these are all the files under build/env/jpf... java/io/File.class java/io/RandomAccessFile$DataRepresentation.class java/io/RandomAccessFile.class java/lang/Class.class java/lang/StackTraceElement.class java/lang/Thread.class java/lang/ref/Reference.class java/lang/ref/ReferenceQueue.class java/lang/ref/WeakReference.class java/security/AccessController.class sun/misc/AtomicLong.class I'll have to check at home on Windows later. So am I missing some class files? I just re-ran "run-tests" (after removing TestAssert) and all the tests ran and passed. But still no Object class under the path you mentioned (but I do have this file: build/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.class). I noticed this in build.xml: "NOTE - some targets might be skipped if you don't have a 'local.properties' file" - I don't have that file. I believe I already tried this but I'll also add build/env/jvm to the classpath and try again. Shane. |
|
From: Arkadeb G. <ar...@gm...> - 2006-04-12 04:11:17
|
Hi Shane,
I was also getting the same problem when i tried to set JPF on eclipse.
The error is reported if you have not build everything properly ... a set o=
f
instructions i followed that led to correct working on Eclipse are as
follows:
(you may try once more)
- arko
JPF on Eclipse
1. Go to the menu "*File-Import-Checkout projects from CVS*" item
*To create new repository location:*
Host: cvs.sourceforge.net
Repository path: /cvsroot/javapathfinder
User: Anonymous
Password: *no password is required*
Connection type; pserver
Use Default Port
1. Click "Use specified module name:"
Enter javapathfinder
Click "Next"
1. Select "Check out as a project configured using the New Project
Wizard" *(very important)*
Cick "Next"
1. Click the tag "HEAD" and click "Next"
2. A "New Project" box should appear. Select the "Java Project" wizard
and click "Next"
3. Give the project a name (javapathfinder is a sensible one)
Select "Create project in workspace"
Select "Create separate source and output folders"
DO NOT click the next button yet
1. Click the "Configure Defaults" button
Enter 'src' in the "Source folder name"
Click 'Ok'
1. Hit "next"
2. Next add the external jar files:
bcel.jar, fast-MD5.jar, xercesImpl.jar, and cml-apis.jar
1. Set default output folder to javapathfinder/build/jpf
2. Click "Finish" and wait.
1. After checkout is complete, right click build.xml.
Select "Ant build=85" from "Run".
From "Check targets to execute" slect "compile-examples"
Don't change the any other settings
Hit "Run"
1. Hit Refresh on the project =85
Make sure you have the following directories:
build/env/jpf
build/env/jvm
build/examples
1. How to run the HelloWorld.java example ?
In the run configuration:
In Main: project: javapathfinder, main class: gov.nasa.jpf.JPF
In Arguments: -show HelloWorld, check out "Use default working
directory"
In Classpath: add build\env\jpf, \build\env\jvm and \build\examples
Hit "Run" button.
|
|
From: Adam K. <ak...@MI...> - 2006-04-12 02:23:25
|
Shane, I had the same thing on Windows. On Unix (i use debian linux), the ant build works, once you use JDK 1.4 and remove the AssertTest, because it hangs. hth /adam Shane Davison wrote: > > Willem, > > I cleaned everything out and restarted using JDK 1.4.2_08 but (eventually) > got the same results. I tried adding the flag below (which I believe is > also > specified [correctly] in the default.properties file) and got the same > thing... > > error during VM runtime initialization: > uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError: > java.lang.Object.registerNatives (no peer) > at java.lang.Object.<clinit>(java/lang/Object.java:24) > > If I run the cmd without my app and without the extra flag, I get the help > output. But if I run it without my app but with the config option, I don't > see any output (which seems strange). > > Anyway, I've spent quite a bit of time already so I may just need to > move on. > > Thanks, > Shane. > > ps. It never really worked - I just got further (or at least a > different error) > when running from the root dir. Even the ant build tests hung (at least on > WinXP - I didn't try on Solaris). > > > > > ------------------------------------------------------- > This SF.Net email is sponsored by xPML, a groundbreaking scripting language > that extends applications into web and mobile media. Attend the live > webcast > and join the prime developer group breaking into this new coding territory! > http://sel.as-us.falkag.net/sel?cmd=lnk&kid=110944&bid=241720&dat=121642 > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user |
|
From: Shane D. <sha...@ho...> - 2006-04-11 23:42:13
|
Willem,
I cleaned everything out and restarted using JDK 1.4.2_08 but (eventually)
got the same results. I tried adding the flag below (which I believe is
also
specified [correctly] in the default.properties file) and got the same
thing...
error during VM runtime initialization:
uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError:
java.lang.Object.registerNatives (no peer)
at java.lang.Object.<clinit>(java/lang/Object.java:24)
If I run the cmd without my app and without the extra flag, I get the help
output. But if I run it without my app but with the config option, I don't
see any output (which seems strange).
Anyway, I've spent quite a bit of time already so I may just need to move
on.
Thanks,
Shane.
ps. It never really worked - I just got further (or at least a different
error)
when running from the root dir. Even the ant build tests hung (at least on
WinXP - I didn't try on Solaris).
|
|
From: Shane D. <sha...@ho...> - 2006-04-11 21:52:32
|
Hi Willem, Thanks for your message. I did get an error about vm.bootclasspath prior to this but it looked like it was set correctly in the config/properties files (I think I got past that one before by running from the JPF install/home dir). I tried again by adding that location to my regular classpath but got the same error. I also tried appending and prepending the location to -Xbootclasspath but there was no change (for the former) and an internal hot spot error in the latter. So maybe this is a 1.5 issue. I'll try with 1.4.2. Btw, most of this was from the cmd line but I also tried with NetBeans (and did read the page on how to set things up but still couldn't get it working from there either). Shane. >It looks to be that your vm.bootclasspath is not set correctly, since it >seems that JPF is not finding the peer classes that override some of the >Java lib classes. It should point to build/env/jpf. If you are in Eclipse >just add this folder to your classpath in the run-script. > >BTW, JPF and 1.5 is not best of friends - we will release a 1.5 compatible >version in the next week or two. To be on the safe side you might like to >use 1.4. |
|
From: Willem V. <wv...@em...> - 2006-04-11 15:31:52
|
Hi Shane, It looks to be that your vm.bootclasspath is not set correctly, since it seems that JPF is not finding the peer classes that override some of the Java lib classes. It should point to build/env/jpf. If you are in Eclipse just add this folder to your classpath in the run-script. BTW, JPF and 1.5 is not best of friends - we will release a 1.5 compatible version in the next week or two. To be on the safe side you might like to use 1.4. Bye, Willem ----- Original Message ----- From: "Shane Davison" <sha...@ho...> To: <jav...@li...> Sent: Tuesday, April 11, 2006 12:57 AM Subject: [Javapathfinder-user] java.lang.UnsatisfiedLinkError (no peer) > > Hello, > > I can't seem to get past this error... > > error during VM runtime initialization: > uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError: > java.lang > .Object.registerNatives (no peer) > at java.lang.Object.<clinit>(java\lang\Object.java:24) > > I've tried at work (Solaris) and at home (WinXP), both using JDK 1.5_06, > and with > 2 different apps (one very complicated, the other not so much). They run > fine on > their own. I searched Google (nothing) and this list archives and > although there were > a few posts about this (I think one was in the past day or so), I didn't > understand how > to fix the issue. > > I'm using the default.properties file (unedited), starting from the JPF > root dir, tried > setting different classpaths, copying sources over, etc, etc. > > Any ideas? Is there a log or some other way I can provide more info? > > > > > ------------------------------------------------------- > This SF.Net email is sponsored by xPML, a groundbreaking scripting > language > that extends applications into web and mobile media. Attend the live > webcast > and join the prime developer group breaking into this new coding > territory! > http://sel.as-us.falkag.net/sel?cmd=lnk&kid=110944&bid=241720&dat=121642 > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user |
|
From: Shane D. <sha...@ho...> - 2006-04-11 09:33:36
|
Hello,
I can't seem to get past this error...
error during VM runtime initialization:
uncaught exception in thread main #0 : java.lang.UnsatisfiedLinkError:
java.lang
.Object.registerNatives (no peer)
at java.lang.Object.<clinit>(java\lang\Object.java:24)
I've tried at work (Solaris) and at home (WinXP), both using JDK 1.5_06, and
with
2 different apps (one very complicated, the other not so much). They run
fine on
their own. I searched Google (nothing) and this list archives and although
there were
a few posts about this (I think one was in the past day or so), I didn't
understand how
to fix the issue.
I'm using the default.properties file (unedited), starting from the JPF root
dir, tried
setting different classpaths, copying sources over, etc, etc.
Any ideas? Is there a log or some other way I can provide more info?
|
68 messages has been excluded from this view by a project administrator.
