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: harry h. <har...@ho...> - 2006-03-13 15:18:03
|
Hi,
I am the new to the Java pathfinder. I successfully installed it on the
Linux. The java version is 1.5 in the machine. I run the deadlock example in
the /examples directory following the instruction of readme in that folder.
The "java deadlock.Deadlock" passed and give me the output like in below :
=============
B.foo() was called
B cycle start
A cycle end
A.foo() was called
A cycle start
B cycle end
B.foo() was called
=============
However, when I executed "jpf deadlock.Deadlock", there are exceptions
thrown :
========
java.lang.RuntimeException: Unknown or invalid constant type at 99
at org.apache.bcel.generic.LDC.getType(LDC.java:148)
at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:51)
at gov.nasa.jpf.jvm.bytecode.Instruction.init(Instruction.java:221)
at
gov.nasa.jpf.jvm.bytecode.Instruction.create(Instruction.java:153)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:628)
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:1170)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:350)
at gov.nasa.jpf.jvm.bytecode.NEW.execute(NEW.java:43)
at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
JPF exception, terminating: class java.lang.StringIndexOutOfBoundsException:
String index out of range: -3
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:163)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:628)
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:1170)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:350)
at gov.nasa.jpf.jvm.bytecode.NEW.execute(NEW.java:43)
at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
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:163)
at gov.nasa.jpf.jvm.MethodInfo.loadCode(MethodInfo.java:628)
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:1170)
at gov.nasa.jpf.jvm.ClassInfo.<init>(ClassInfo.java:252)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:350)
at gov.nasa.jpf.jvm.bytecode.NEW.execute(NEW.java:43)
at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
gov.nasa.jpf.JPFException: class java.lang.StringIndexOutOfBoundsException:
String index out of range: -3
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1154)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
============
Can someone give me some advices and how to fix it ?
Thanks.
Harry
|
|
From: zuo j. <zu...@pk...> - 2006-03-01 13:31:45
|
Hi, a new trouble came out. A NullPointer Exception was issued from deep
inside jpf. At the beginning, I thought that the NullPointer might happen
somewhere in my application. So, I set up many points to print out how my
app behaved. In this way, I narrowed down to the place where the exception
happened. But I could not find any reference to a null pointer there.
Instead, my app just stopped there. Superficially, there seemed nothing
wrong with the piece of code.
Can anybody give me a hint? Though I know the problem is so subtle that it
may be difficult to find out the reason. I just paste the error message
below. Sorry for its length.
J. H. Zuo
$ bin/jpf model.MailVerifier > result
JPF exception, terminating: class java.lang.NullPointerException: null
java.lang.NullPointerException
at gov.nasa.jpf.jvm.DynamicArea.markRecursive(DynamicArea.java:310)
at gov.nasa.jpf.jvm.DynamicArea.analyzeHeap(DynamicArea.java:161)
at
gov.nasa.jpf.jvm.ElementInfo.updateReachability(ElementInfo.java:346
at
gov.nasa.jpf.jvm.ElementInfo.setReferenceField(ElementInfo.java:367)
at gov.nasa.jpf.jvm.bytecode.PUTFIELD.execute(PUTFIELD.java:63)
at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
java.lang.NullPointerException
at gov.nasa.jpf.jvm.DynamicArea.markRecursive(DynamicArea.java:310)
at gov.nasa.jpf.jvm.DynamicArea.analyzeHeap(DynamicArea.java:161)
at
gov.nasa.jpf.jvm.ElementInfo.updateReachability(ElementInfo.java:346
at
gov.nasa.jpf.jvm.ElementInfo.setReferenceField(ElementInfo.java:367)
at gov.nasa.jpf.jvm.bytecode.PUTFIELD.execute(PUTFIELD.java:63)
at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1505)
at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2081)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1111)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
gov.nasa.jpf.JPFException: class java.lang.NullPointerException: null
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1154)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
at gov.nasa.jpf.jvm.JVM.tryAgain(JVM.java:1064)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1146)
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:308)
at gov.nasa.jpf.JPF.main(JPF.java:238)
|
|
From: Willem V. <wv...@em...> - 2006-02-28 23:22:10
|
Hi All, Sorry for abusing the list, but we set up a Frappr group to give everyone the chance to let the rest of us know who are using JPF. Please join us at: http://www.frappr.com/jpfusers 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 |
|
From: zuo j. <zu...@pk...> - 2006-02-24 09:55:42
|
Hi, I finally fix the problem. In fact, it is because jpf does not know where to find the native peer class although the native peer class and model class reside at the same directory. To make jpf be aware of that, just set CLASSPATH to point to the top package where the native peer class resides. One thought: Is it more natural to let jpf search for native peer classes automatically? After all, native peers and model classes are usually under the same package. |
|
From: zuo j. <zu...@pk...> - 2006-02-23 12:43:13
|
First, I would like to thank Willem. I followed his suggestion to write =
a
peer class. But when I run jpf, it=A1=AFs reported that no peer is =
found. The
following is the excerpt of my program.
=20
Model class:
package model;
public class ScenarioManager {
native private boolean hasEquivalentPeer(Scenario scen);
public boolean hasMatch(Message msg) {
Scenario scen =3D new Scenario();
=A1=AD
return hasEquivalentPeer(scen);
}
}
=20
Peer class:
public class JPF_model_ScenarioManager {
public static TreeSet scenarios;
public static boolean hasEquivalentPeer__Lmodel_Scenario_2(MJIEnv env, =
int
robj, int scenRef) {
Scenario scen =3D reconstructScenario(env, scenRef);
if (scenarios.contains(scen)) return true;
else {
scenarios.add(scen);
return false;
}
}
=20
When I run jpf, an error message is displayed, which is:
java.lang.UnsatisfiedLinkError: model.ScenarioManager.hasEquivalentPeer =
(no
peer)
=20
So, what=A1=AFs wrong? Is there anything that misses my attention?
Thanks again!
=20
J. H. Zuo
|
|
From: zuo j. <zu...@pk...> - 2006-02-21 11:30:56
|
Hello, I encounter a problem with using jpf and have to request for help.
My program has a test driver class User that models a user who generates
mails in different scenarios. This is achieved by non-deterministically
setting the receiver field.
class User {
...
public void writeMail() {
Message msg = Message.create();
...
receiver = pickAddress();
msg.setReceiver(receiver);
agent.messageGenerated(msg);
}
}
As the scenarios are too many, I need to make reductions before processing
the newly generated message by analyzing if it is equivalent with some
message that has been generated and processed before. If the newly generated
message has equivalent peers it will be omitted.
To do so, the previously generated messages need to be stored. But I
noticed that when jpf backtracks and generates a new message, the fields of
all objects will be restored to their original states. Thus, all the
previously generated messages cannot be stored.
I wanted to use SearchListener and VMListener. After I looking at their
source files I found that they do not provide the values of the variables of
complex types. How can I store and access the variables that are related
with the previous scenario?
Thanks in advance!
J. H. Zuo
|
|
From: John P. <joh...@gm...> - 2006-02-21 04:09:19
|
Hi Pratibha, it sounds like it may be having trouble finding your java installation - tr= y running it as >java gov.nasa.jpf.jvm.JPF and see what you get. John On 2/17/06, Pratibha Permandla <pra...@gm...> wrote: > > HI, > > I am totally new to JPF. I have installed JPF . The ant run-tests works > fine and I have set all the classpath and path variable. But when I run > bin/jpf : it says command not found in TCSH shell. WHen I do it Bash shel= l, > it says bad interpretor: no such file or directory. Could somebody please > give me some pointers regarding this. > > Thanks very much > > |
|
From: Muhammad A. S. <muh...@gm...> - 2006-02-18 10:09:20
|
It's the famous newline character (CR/LF) problem with the packages put at sourceforge. You need to convert the file format from Windows to *nix. Alternatively, checkout everything from CVS. Here is how: http://jaywalker.blogspot.com/2005_07_01_jaywalker_archive.html Best Regards, Muhammad Ali On 2/18/06, Pratibha Permandla <pra...@gm...> wrote: > HI, > > I am totally new to JPF. I have installed JPF . The ant run-tests work= s > fine and I have set all the classpath and path variable. But when I run > bin/jpf : it says command not found in TCSH shell. WHen I do it Bash shel= l, > it says bad interpretor: no such file or directory. Could somebody please > give me some pointers regarding this. > > Thanks very much > > |
|
From: Pratibha P. <pra...@gm...> - 2006-02-18 02:14:02
|
HI, I am totally new to JPF. I have installed JPF . The ant run-tests works fine and I have set all the classpath and path variable. But when I run bin/jpf : it says command not found in TCSH shell. WHen I do it Bash shell, it says bad interpretor: no such file or directory. Could somebody please give me some pointers regarding this. Thanks very much |
|
From: Mark S. <ma...@or...> - 2006-02-08 02:14:18
|
I am trying to run the Java pathfinder on a Linux system (Fedora Core 2) running java version 1.4.2_05. When I follow the instructions to try to build the system, the ant compile-env-pf step fails with three errors, all for files in env/jpf/java/lang: in Class.java, line 44 - duplicate definition 'String name' in Thread.java, lines 38 and 39: type ThreadLocal.ThreadLocalMap not found Any idea what the problem might be? Mark Saaltink |
|
From: Todd W. <tc...@ks...> - 2006-01-13 16:14:55
|
I am trying to evaluate a system based upon a Replicated Workers pattern
and was confused by the output that JPF generated for me. It dumps a
stack trace but then reports "No Errors Found". Does this mean that it
did find an error? Or maybe the stack trace is associated with the
warning printed?
I also found this in several other, shorter running cases of this
application (using different command line arguments that control the
size of the system). I also found that jpf printed those warnings for
some of the other command line argument combinations but did not print
stack traces.
I would be happy to provide the source for the example if it would help.
I have included the command line that I ran and the output that was
generated below:
shawnee$ time jpf apps.AdaptiveQuadrature.Main 4 1 0.0 30.0 5e-3
Warning: unprotected field access of:
ca....@16...eCoord in thread:
"Thread-0" ca/replicatedworkers/ReplicatedWorkers.java:270
sync-detection assumed to be protected by:
ca.replicatedworkers.ReplicatedWorkers@160
found to be protected by: {}
>>> re-run without '-sync-detection' <<<
------------------------------------ thread stacks
Thread: main
at java.lang.Object.wait(java/lang/Object.java:429)
at
ca.replicatedworkers.Coordinator.mainAwaitTerminate(ca/replicatedworkers/ReplicatedWorkers.java:173)
at
ca.replicatedworkers.ReplicatedWorkers.execute(ca/replicatedworkers/ReplicatedWorkers.java:118)
at
apps.AdaptiveQuadrature.Main.main(apps/AdaptiveQuadrature/Main.java:79)
Thread: Thread-0
at java.lang.Object.wait(java/lang/Object.java:429)
at
ca.replicatedworkers.Coordinator.take(ca/replicatedworkers/ReplicatedWorkers.java:196)
at
ca.replicatedworkers.Worker.run(ca/replicatedworkers/ReplicatedWorkers.java:270)
Thread: Thread-1
at
ca.replicatedworkers.Worker.run(ca/replicatedworkers/ReplicatedWorkers.java:266)
Thread: Thread-2
at java.lang.Object.wait(java/lang/Object.java:429)
at
ca.replicatedworkers.Coordinator.take(ca/replicatedworkers/ReplicatedWorkers.java:196)
at
ca.replicatedworkers.Worker.run(ca/replicatedworkers/ReplicatedWorkers.java:270)
Thread: Thread-3
at
ca.replicatedworkers.Worker.run(ca/replicatedworkers/ReplicatedWorkers.java:270)
===================================
No Errors Found
===================================
real 632m40.924s
user 632m30.266s
sys 0m3.307s
Any guidance would be appreciated,
Todd Wallentine
ps
Just in case it helps, here are some stats about the environment that
this is running in:
1) Sun dual-core Opteron 87shawnee$ java -version
2) Java version (java -version)
java version "1.4.2-02"
Java(TM) 2 Runtime Environment, Standard Edition (build Blackdown-1.4.2-02)
Java HotSpot(TM) 64-Bit Server VM (build Blackdown-1.4.2-02, mixed
mode)5, 32G RAM
3) Built from CVS on Jan 6, 2006
|
|
From: Willem V. <wv...@em...> - 2005-12-19 17:38:22
|
The implementation in the Verify class is empty, since that is just used as a trap for the model checker to react to - if you look in the JPF_gov_nasa_jpf_jvm_Verify.java file in the same directory (i.e. the native peer of the Verify class that actually gets executed) you'll see the true body of the ignoreIf method. If you still don't believe me that it really prunes the state space put an assert false right after a ignoreif true and see if it ever gets triggered :-) -- 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 zuo jihong Sent: Sunday, December 18, 2005 10:19 PM To: Jav...@li... Subject: [Javapathfinder-user] Verify.ignoreIf does not work Hi, I encounter a problem when instrumenting code with Verify. The code is to simulate a user action. For example, Address item = pickAddress(); if (item != null) { Verify.ignoreIf(item.isEqual(Address.Remailer)); forwMsg.setForwardItem(item); } According to the doc on the web, Verify.ignoreIf can prune state search. "If the provided expression evaluates to true, JPF does not continue to execute the current path, and backtracks to the previous non-deterministic choice point." However, it is not the fact. As I traced into the execution I found that Verify.ignoreIf() is only an empty function. Nothing happens when the expression evaluates to true. Then, how can I implement search pruning and backtracking in my code? J.H. Zuo |
|
From: zuo j. <zu...@pk...> - 2005-12-19 06:39:29
|
Hi, I encounter a problem when instrumenting code with Verify. The code =
is
to simulate a user action. For example,=20
Address item =3D pickAddress();
if (item !=3D null) {
Verify.ignoreIf(item.isEqual(Address.Remailer));
forwMsg.setForwardItem(item);
}
=20
According to the doc on the web, Verify.ignoreIf can prune state search.
=A1=B0If the provided expression evaluates to true, JPF does not =
continue to
execute the current path, and backtracks to the previous =
non-deterministic
choice point.=A1=B1
However, it is not the fact. As I traced into the execution I found that
Verify.ignoreIf() is only an empty function. Nothing happens when the
expression evaluates to true. Then, how can I implement search pruning =
and
backtracking in my code?
=20
J.H. Zuo
|
|
From: zuo j. <zu...@pk...> - 2005-12-07 05:19:11
|
I=A1=AFve fixed the problem. It seems to be caused by the =
incompatibility
between BCEL and JDK. My original JDK is 1.4.1. When I turn to use java =
1.4.
2, all the problems disappear.
=20
J.H. Zuo
_____ =20
=B7=A2=BC=FE=C8=CB: zuo jihong [mailto:zu...@pk...]=20
=B7=A2=CB=CD=CA=B1=BC=E4: 2005=C4=EA12=D4=C26=C8=D5 15:08
=CA=D5=BC=FE=C8=CB: 'Jav...@li...'
=D6=F7=CC=E2: testing of jpf failed
=20
Hi,
I=A1=AFm new to JPF. And when I try to build JPF by typing =A1=B0ant =
run-tests=A1=B1
something wrong would happen. My OS is Windows2000.
In console environment, nothing would appear under =
=A1=B0run-tests=A1=B1 target,
just looking like this:
=A1=AD
compile-env-jvm:
[javac] Compiling 22 source files to
D:\UTILIT~1\jpf\build\env\jvm
=20
compile-env-jpf:
[javac] Compiling 10 source files to
D:\UTILIT~1\jpf\build\env\jpf
=20
compile:
=20
compile-tests:
[javac] Compiling 35 source files to
D:\UTILIT~1\jpf\build\test
=20
run-tests:
=20
BUILD SUCCESSFUL
Total time: 13 seconds
=20
However, when I turn to cygwin environment, testing can happen under
=A1=B0run-tests=A1=B1, but all of the test items failed. Look at the =
excerpt below:
run-tests:
[echo] --- running Junit tests from build/test..
[junit] Running gov.nasa.jpf.jvm.TestArrayJPF
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray =
test2DArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray
test2DStringArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray testAoBX
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray
testCharArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray =
testIntArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray
testStringArray
[junit] Tests run: 6, Failures: 6, Errors: 0, Time elapsed: 0.703 =
sec
[junit] TEST gov.nasa.jpf.jvm.TestArrayJPF FAILED
[junit] Running gov.nasa.jpf.jvm.TestAssertJPF
[junit] running jpf with args: gov.nasa.jpf.jvm.TestAssert =
testAssert
[junit] running jpf with args: +vm.enable_assertions=3D
gov.nasa.jpf.jvm.TestAssert testAssert
[junit] Tests run: 2, Failures: 2, Errors: 0, Time elapsed: 0.375 sec
[junit] TEST gov.nasa.jpf.jvm.TestAssertJPF FAILED
=A1=AD
=20
I am using java1.4.1. And the environment variable is:
CLASSPATH =3D ./build-tools/lib/ant.jar : ./build-tools/lib/junit.jar :
./lib/bcel.jar : ./lib/fast-MD5.jar : ./lib/xercesImpl.jar : =
./lib/xml-apis.
jar
=20
Although the jpf has been compiled, it cannot work properly. When I type
=A1=B0bin/jpf =A8Cshow=A1=B1 it can show dictionary correctly. For =
example:=20
$ bin/jpf -show
=A1=AD
vm.bootclasspath =3D bin/../build/env/jpf
vm.check_fp =3D false
vm.check_fp_compare =3D true
vm.class =3D gov.nasa.jpf.jvm.JVM
vm.classpath =3D build/examples
=A1=AD
=20
But when I type =A1=B0bin/jpf HelloWorld=A1=B1 something wrong happened:
$ bin/jpf HelloWorld
java.lang.NoSuchMethodError:
org.apache.bcel.classfile.JavaClass.setRepository(Lorg/apache/bcel/util/R=
epo
sitory;)V
at
org.apache.bcel.util.SyntheticRepository.storeClass(SyntheticRepository.j=
ava
:82)
at
org.apache.bcel.util.SyntheticRepository.loadClass(SyntheticRepository.ja=
va:
172)
at
org.apache.bcel.util.SyntheticRepository.loadClass(SyntheticRepository.ja=
va:
126)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:339)
at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1368)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:285)
at gov.nasa.jpf.JPF.run(JPF.java:307)
at gov.nasa.jpf.JPF.main(JPF.java:238)
=20
The error appeared in both cygwin environment and console environment. I
cannot figure out what=A1=AFs the reason. So can anybody help me? Many =
thanks!
=20
J.H. Zuo
|
|
From: Muhammad A. S. <muh...@gm...> - 2005-12-06 12:50:50
|
The last error is given by BCEL and it happened with me as well when I
used Java 1.5 with the latest release of BCEL. Please make sure that
you are using JDK 1.4 ("java -version") and if possible, use the BCEL
library that is available in the Javapathfinder external libraries.
Hope this fixes the problem.
/Ali
Chalmers University of Technology,
Sweden
> But when I type "bin/jpf HelloWorld" something wrong happened:
>
> $ bin/jpf HelloWorld
>
> java.lang.NoSuchMethodError:
> org.apache.bcel.classfile.JavaClass.setRepository(Lorg/apache/bcel/util/R=
epository;)V
>
> at
> org.apache.bcel.util.SyntheticRepository.storeClass(SyntheticRepository.j=
ava:82)
>
> at
> org.apache.bcel.util.SyntheticRepository.loadClass(SyntheticRepository.ja=
va:172)
>
> at
> org.apache.bcel.util.SyntheticRepository.loadClass(SyntheticRepository.ja=
va:126)
>
> at
> gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:339)
>
> at
> gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1368)
>
> at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:285)
>
> at gov.nasa.jpf.JPF.run(JPF.java:307)
>
> at gov.nasa.jpf.JPF.main(JPF.java:238)
|
|
From: zuo j. <zu...@pk...> - 2005-12-06 07:36:14
|
Hi,
I=A1=AFm new to JPF. And when I try to build JPF by typing =A1=B0ant =
run-tests=A1=B1
something wrong would happen. My OS is Windows2000.
In console environment, nothing would appear under =
=A1=B0run-tests=A1=B1 target,
just looking like this:
=A1=AD
compile-env-jvm:
[javac] Compiling 22 source files to
D:\UTILIT~1\jpf\build\env\jvm
=20
compile-env-jpf:
[javac] Compiling 10 source files to
D:\UTILIT~1\jpf\build\env\jpf
=20
compile:
=20
compile-tests:
[javac] Compiling 35 source files to
D:\UTILIT~1\jpf\build\test
=20
run-tests:
=20
BUILD SUCCESSFUL
Total time: 13 seconds
=20
However, when I turn to cygwin environment, testing can happen under
=A1=B0run-tests=A1=B1, but all of the test items failed. Look at the =
excerpt below:
run-tests:
[echo] --- running Junit tests from build/test..
[junit] Running gov.nasa.jpf.jvm.TestArrayJPF
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray =
test2DArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray
test2DStringArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray testAoBX
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray
testCharArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray =
testIntArray
[junit] running jpf with args: gov.nasa.jpf.jvm.TestArray
testStringArray
[junit] Tests run: 6, Failures: 6, Errors: 0, Time elapsed: 0.703 =
sec
[junit] TEST gov.nasa.jpf.jvm.TestArrayJPF FAILED
[junit] Running gov.nasa.jpf.jvm.TestAssertJPF
[junit] running jpf with args: gov.nasa.jpf.jvm.TestAssert =
testAssert
[junit] running jpf with args: +vm.enable_assertions=3D
gov.nasa.jpf.jvm.TestAssert testAssert
[junit] Tests run: 2, Failures: 2, Errors: 0, Time elapsed: 0.375 sec
[junit] TEST gov.nasa.jpf.jvm.TestAssertJPF FAILED
=A1=AD
=20
I am using java1.4.1. And the environment variable is:
CLASSPATH =3D ./build-tools/lib/ant.jar : ./build-tools/lib/junit.jar :
./lib/bcel.jar : ./lib/fast-MD5.jar : ./lib/xercesImpl.jar : =
./lib/xml-apis.
jar
=20
Although the jpf has been compiled, it cannot work properly. When I type
=A1=B0bin/jpf =A8Cshow=A1=B1 it can show dictionary correctly. For =
example:=20
$ bin/jpf -show
=A1=AD
vm.bootclasspath =3D bin/../build/env/jpf
vm.check_fp =3D false
vm.check_fp_compare =3D true
vm.class =3D gov.nasa.jpf.jvm.JVM
vm.classpath =3D build/examples
=A1=AD
=20
But when I type =A1=B0bin/jpf HelloWorld=A1=B1 something wrong happened:
$ bin/jpf HelloWorld
java.lang.NoSuchMethodError:
org.apache.bcel.classfile.JavaClass.setRepository(Lorg/apache/bcel/util/R=
epo
sitory;)V
at
org.apache.bcel.util.SyntheticRepository.storeClass(SyntheticRepository.j=
ava
:82)
at
org.apache.bcel.util.SyntheticRepository.loadClass(SyntheticRepository.ja=
va:
172)
at
org.apache.bcel.util.SyntheticRepository.loadClass(SyntheticRepository.ja=
va:
126)
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:339)
at gov.nasa.jpf.jvm.JVM.loadStartupClasses(JVM.java:1368)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:285)
at gov.nasa.jpf.JPF.run(JPF.java:307)
at gov.nasa.jpf.JPF.main(JPF.java:238)
=20
The error appeared in both cygwin environment and console environment. I
cannot figure out what=A1=AFs the reason. So can anybody help me? Many =
thanks!
=20
J.H. Zuo
|
|
From: Dusty P. <bu...@gm...> - 2005-11-26 01:49:35
|
On 24/11/05, Willem Visser <wv...@em...> wrote:
> Hi Dusty,
>
> Add a -show to the command line to see which options are being loaded. Yo=
u
> don't need to do a -c option if you add it to jpf.properties (it loads th=
at
> by default). Actually also add a +config.level=3Dconfig (I think this is =
the
> command) to the command line and that will tell you where the properties
> gets loaded from.
Hi Willem,
I'm still having trouble detecting a race condition. I wrote a simple
test that looks like a race condition:
public class RaceCond {
public int theInt;
public static void main(String[] args) {
RaceCond raceCond =3D new RaceCond();
raceCond.theInt =3D 10;
new t1(raceCond).start();
new t2(raceCond).start();
}
}
class t1 extends Thread {
private RaceCond racer;
public t1(RaceCond blah) {
racer =3D blah;
}
public void run() {
racer.theInt++;
}
}
class t2 is the same as t1, but decrements the value instead.
So I put this in my jpf.properties:
listener =3D gov.nasa.jpf.tools.RaceDetector
When I run it it tells me no errors found, although I think the class
above is an obvious race condition. Am I defining 'race condition' too
simply (I need something more complicated than above?) or am I not
implementing the listener correctly?
Sorry to keep pestering you with these questions. I think I understand
what JPF is doing, but not necessarily how to control it! :-D I've
been browsing through the sources to get a better understanding, but
there are still gaps in my knowledge to actually get started using it.
Thanks again,
Dusty
|
|
From: Willem V. <wv...@em...> - 2005-11-24 16:51:15
|
Hi Dusty, The changes to get 1.5 working is massive, but almost done. Bye, Willem ----- Original Message ----- From: "Dusty Phillips" <bu...@gm...> To: "Willem Visser" <wv...@em...> Cc: <Jav...@li...> Sent: Thursday, November 24, 2005 7:36 AM Subject: Re: [Javapathfinder-user] necessary locks > On 24/11/05, Willem Visser <wv...@em...> wrote: > > Hi Dusty, > > > > Add a -show to the command line to see which options are being loaded. You > > don't need to do a -c option if you add it to jpf.properties (it loads that > > by default). Actually also add a +config.level=config (I think this is the > > command) to the command line and that will tell you where the properties > > gets loaded from. > > Thanks, I will try these options and see what happens. > > > > Also if JPF seems to hang that can definitely be the 1.5 issue - it does go > > into and endless loop if run on 1.5 library code. This will soon be fixed > > but it is not yet in the CVS version. > > Does this mean you have the fix on hand? If so, would it be possible > for me to patch the CVS version to make Java 1.5 work, or is it a > difficult fix modifying many lines of code? > > Thanks once again, > Dusty > |
|
From: Dusty P. <bu...@gm...> - 2005-11-24 15:36:54
|
On 24/11/05, Willem Visser <wv...@em...> wrote: > Hi Dusty, > > Add a -show to the command line to see which options are being loaded. Yo= u > don't need to do a -c option if you add it to jpf.properties (it loads th= at > by default). Actually also add a +config.level=3Dconfig (I think this is = the > command) to the command line and that will tell you where the properties > gets loaded from. Thanks, I will try these options and see what happens. > Also if JPF seems to hang that can definitely be the 1.5 issue - it does = go > into and endless loop if run on 1.5 library code. This will soon be fixed > but it is not yet in the CVS version. Does this mean you have the fix on hand? If so, would it be possible for me to patch the CVS version to make Java 1.5 work, or is it a difficult fix modifying many lines of code? Thanks once again, Dusty |
|
From: Willem V. <wv...@em...> - 2005-11-24 07:14:40
|
Hi Dusty, Add a -show to the command line to see which options are being loaded. You don't need to do a -c option if you add it to jpf.properties (it loads that by default). Actually also add a +config.level=config (I think this is the command) to the command line and that will tell you where the properties gets loaded from. To see progress you should add the SearchMonitor for sure. Also if JPF seems to hang that can definitely be the 1.5 issue - it does go into and endless loop if run on 1.5 library code. This will soon be fixed but it is not yet in the CVS version. Bye, Willem ----- Original Message ----- From: "Dusty Phillips" <bu...@gm...> To: <wv...@em...> Cc: <Jav...@li...> Sent: Wednesday, November 23, 2005 8:27 PM Subject: Re: [Javapathfinder-user] necessary locks > Hi Willem, > > Thanks for the advice. I can tell this is what I want, but I'm not > sure how to make it work. > > I've created a jpf. properties and have added > listener=gov.nasa.jpf.tools.RaceDetector to it. I pass this properties > using jpf -c. Is that all I need to make it work? It doesn't seem to > change anything one way or the other. > > Possibly on a related topic, I frequently run JPF and it doesn't > terminate. I assume the state space is too big, but maybe there is > another problem. I was wondering how I can tell if JPF is making > progress. I tried adding a > search.listener=gov.nasa.jpf.tools.SearchMonitor to my jpf.properties, > but it doesn't seem to add any output. Is this not the tool I want? > > I read on the forum that Java 1.5 and BCEL were not playing well on > July 13 (http://sourceforge.net/forum/forum.php?thread_id=1317153&forum_id=461881). > Is this still the case? Would that be causing my problems? > > I think I'm just having trouble getting started here. :-) > > Thanks, > Dusty > > On 21/11/05, Willem Visser <wv...@em...> wrote: > > Hi Dusty, > > > > Use the RaceDetector listener in the tools directory - it will tell you > > if there is a race violation possible on the queue without the locks. > > > > 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 > > > Dusty Phillips > > > Sent: Saturday, November 19, 2005 2:00 PM > > > To: Jav...@li... > > > Subject: [Javapathfinder-user] necessary locks > > > > > > Hello, > > > > > > I'm just starting to understand how to use Java Pathfinder (got the > > > cvs version working). So far I've been implementing a model and > > > running it in JPF without writing extra properties or using the Verify > > > class, though I intend to add these eventually. > > > > > > I was wondering if it would be possible using JPF to test whether or > > > not a specific lock is needed. For example, I've implemented a > > > concurrently accessible queue with synchronized methods for offering > > > and polling objects. From the design of the rest of the model, I can't > > > tell if this queue is ever actually accesed concurrently. I think that > > > at worst, it may be written by one process while another process is > > > reading it. Is there some way to write a property to test whether or > > > not this happens? > > > > > > This isn't a deadlock issue, so I don't think the default deadlock > > > property will do what I want. I'm not sure where to start when it > > > comes to writing properties or otherwise customizing JPF. > > > > > > Thank you, > > > > > > Dusty > > > > > > > > > ------------------------------------------------------- > > > This SF.Net email is sponsored by the JBoss Inc. Get Certified Today > > > Register for a JBoss Training Course. Free Certification Exam > > > for All Training Attendees Through End of 2005. For more info visit: > > > http://ads.osdn.com/?ad_idv28&alloc_id845&opÌk > > > _______________________________________________ > > > Javapathfinder-user mailing list > > > Jav...@li... > > > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > > > > > > > |
|
From: Dusty P. <bu...@gm...> - 2005-11-24 04:27:58
|
Hi Willem, Thanks for the advice. I can tell this is what I want, but I'm not sure how to make it work. I've created a jpf. properties and have added listener=3Dgov.nasa.jpf.tools.RaceDetector to it. I pass this properties using jpf -c. Is that all I need to make it work? It doesn't seem to change anything one way or the other. Possibly on a related topic, I frequently run JPF and it doesn't terminate. I assume the state space is too big, but maybe there is another problem. I was wondering how I can tell if JPF is making progress. I tried adding a search.listener=3Dgov.nasa.jpf.tools.SearchMonitor to my jpf.properties, but it doesn't seem to add any output. Is this not the tool I want? I read on the forum that Java 1.5 and BCEL were not playing well on July 13 (http://sourceforge.net/forum/forum.php?thread_id=3D1317153&forum_i= d=3D461881). Is this still the case? Would that be causing my problems? I think I'm just having trouble getting started here. :-) Thanks, Dusty On 21/11/05, Willem Visser <wv...@em...> wrote: > Hi Dusty, > > Use the RaceDetector listener in the tools directory - it will tell you > if there is a race violation possible on the queue without the locks. > > 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 > > Dusty Phillips > > Sent: Saturday, November 19, 2005 2:00 PM > > To: Jav...@li... > > Subject: [Javapathfinder-user] necessary locks > > > > Hello, > > > > I'm just starting to understand how to use Java Pathfinder (got the > > cvs version working). So far I've been implementing a model and > > running it in JPF without writing extra properties or using the Verify > > class, though I intend to add these eventually. > > > > I was wondering if it would be possible using JPF to test whether or > > not a specific lock is needed. For example, I've implemented a > > concurrently accessible queue with synchronized methods for offering > > and polling objects. From the design of the rest of the model, I can't > > tell if this queue is ever actually accesed concurrently. I think that > > at worst, it may be written by one process while another process is > > reading it. Is there some way to write a property to test whether or > > not this happens? > > > > This isn't a deadlock issue, so I don't think the default deadlock > > property will do what I want. I'm not sure where to start when it > > comes to writing properties or otherwise customizing JPF. > > > > Thank you, > > > > Dusty > > > > > > ------------------------------------------------------- > > This SF.Net email is sponsored by the JBoss Inc. Get Certified Today > > Register for a JBoss Training Course. Free Certification Exam > > for All Training Attendees Through End of 2005. For more info visit: > > http://ads.osdn.com/?ad_idv28&alloc_id=16845&op=CCk > > _______________________________________________ > > Javapathfinder-user mailing list > > Jav...@li... > > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > > > |
|
From: Willem V. <wv...@em...> - 2005-11-21 18:29:00
|
Hi Dusty, Use the RaceDetector listener in the tools directory - it will tell you if there is a race violation possible on the queue without the locks.=20 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 > Dusty Phillips > Sent: Saturday, November 19, 2005 2:00 PM > To: Jav...@li... > Subject: [Javapathfinder-user] necessary locks >=20 > Hello, >=20 > I'm just starting to understand how to use Java Pathfinder (got the > cvs version working). So far I've been implementing a model and > running it in JPF without writing extra properties or using the Verify > class, though I intend to add these eventually. >=20 > I was wondering if it would be possible using JPF to test whether or > not a specific lock is needed. For example, I've implemented a > concurrently accessible queue with synchronized methods for offering > and polling objects. From the design of the rest of the model, I can't > tell if this queue is ever actually accesed concurrently. I think that > at worst, it may be written by one process while another process is > reading it. Is there some way to write a property to test whether or > not this happens? >=20 > This isn't a deadlock issue, so I don't think the default deadlock > property will do what I want. I'm not sure where to start when it > comes to writing properties or otherwise customizing JPF. >=20 > Thank you, >=20 > Dusty >=20 >=20 > ------------------------------------------------------- > This SF.Net email is sponsored by the JBoss Inc. Get Certified Today > Register for a JBoss Training Course. Free Certification Exam > for All Training Attendees Through End of 2005. For more info visit: > http://ads.osdn.com/?ad_idv28&alloc_id=16845&op=CCk > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user |
|
From: Dusty P. <bu...@gm...> - 2005-11-19 22:00:05
|
Hello, I'm just starting to understand how to use Java Pathfinder (got the cvs version working). So far I've been implementing a model and running it in JPF without writing extra properties or using the Verify class, though I intend to add these eventually. I was wondering if it would be possible using JPF to test whether or not a specific lock is needed. For example, I've implemented a concurrently accessible queue with synchronized methods for offering and polling objects. From the design of the rest of the model, I can't tell if this queue is ever actually accesed concurrently. I think that at worst, it may be written by one process while another process is reading it. Is there some way to write a property to test whether or not this happens? This isn't a deadlock issue, so I don't think the default deadlock property will do what I want. I'm not sure where to start when it comes to writing properties or otherwise customizing JPF. Thank you, Dusty |
|
From: John P. <joh...@na...> - 2005-11-18 05:37:18
|
Hi Harry, I'm assuming you have gotten JPF to build in Eclipse. if not, look in the JPF Help forum. to run JPF in Eclipse, use this as a Run configuration: project: javapathfinder main class: gov.nasa.jpf.jvm.JPF arguments: -show HelloWorld the classpath must include: ../build/jpf ../build/examples ../build/env/jpf ../build/env/jvm John harry huang wrote: > Hi, > > I am a new user of java PathFinder. I download the Java pathfinder and > install it on the Eclipse. But How can I use the java pathfinder in the > Eclipse environment to verfiy my program. For instance, how to verifiy > the simple class -- HelloWorld.class in the examples directory ? > > Thanks, > Harry > > > > > ------------------------------------------------------- > This SF.Net email is sponsored by the JBoss Inc. Get Certified Today > Register for a JBoss Training Course. Free Certification Exam > for All Training Attendees Through End of 2005. For more info visit: > http://ads.osdn.com/?ad_id=7628&alloc_id=16845&op=click > _______________________________________________ > 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 |
|
From: John P. <joh...@na...> - 2005-11-17 07:41:36
|
Hi Brandon, I don't think you are doing anything wrong. We had a bug with static member access from subclasses which was (allegedly) fixed (by me) on 10/16 and checked into CVS. if you are running the jpf-source-1.0a release, it will still have the bug. the fix was just to a couple of files (GETSTATIC and SETSTATIC in the src/...jpf/jvm/bytecode directory.) you can grab it from the CVS browser, or i can email it to you. if you are running from a recent CVS version, you may have found another problem (or a problem with the fix). if this is the case, it would be great if you could send source or byte code. if this is not possible, a brief description of the static variables in the program might suffice. thanks, John Brandon M wrote: > I can successfully run bin/jpf against > examples/HelloWorld.java, with no problems. I am now > attempting to run jpf against some of my own class > files. I am getting a NullPointerException each time > I run jpf <myClassName>. Below is the stack trace, > along with my parameter settings: > > STACK TRACE > =========== > JPF exception, terminating: class > java.lang.NullPointerException: null > > java.lang.NullPointerException > at > gov.nasa.jpf.jvm.ElementInfo.checkFieldInfo(ElementInfo.java:462) > at > gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:471) > at > gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:41) > at > gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1490) > at > gov.nasa.jpf.jvm.ThreadInfo.executeMethod(ThreadInfo.java:1522) > at > gov.nasa.jpf.jvm.ClassInfo.initializeClass(ClassInfo.java:665) > at > gov.nasa.jpf.jvm.StaticArea.newClass(StaticArea.java:160) > at > gov.nasa.jpf.jvm.StaticArea.get(StaticArea.java:62) > at > gov.nasa.jpf.jvm.ClassInfo.getClassObjectRef(ClassInfo.java:368) > at > gov.nasa.jpf.jvm.bytecode.INVOKESTATIC.isSchedulingRelevant(INVOKESTATIC.java:102) > at > gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2126) > at > gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1546) > at > gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:268) > at gov.nasa.jpf.jvm.JVM.forward(JVM.java:997) > at > gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340) > at > gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84) > at gov.nasa.jpf.JPF.run(JPF.java:308) > at gov.nasa.jpf.JPF.main(JPF.java:238) > java.lang.NullPointerException > at > gov.nasa.jpf.jvm.ElementInfo.checkFieldInfo(ElementInfo.java:462) > at > gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:471) > at > gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:41) > at > gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1490) > at > gov.nasa.jpf.jvm.ThreadInfo.executeMethod(ThreadInfo.java:1522) > at > gov.nasa.jpf.jvm.ClassInfo.initializeClass(ClassInfo.java:665) > at > gov.nasa.jpf.jvm.StaticArea.newClass(StaticArea.java:160) > at > gov.nasa.jpf.jvm.StaticArea.get(StaticArea.java:62) > at > gov.nasa.jpf.jvm.ClassInfo.getClassObjectRef(ClassInfo.java:368) > at > gov.nasa.jpf.jvm.bytecode.INVOKESTATIC.isSchedulingRelevant(INVOKESTATIC.java:102) > at > gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2126) > at > gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1546) > at > gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:268) > at gov.nasa.jpf.jvm.JVM.forward(JVM.java:997) > at > gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340) > at > gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84) > at gov.nasa.jpf.JPF.run(JPF.java:308) > at gov.nasa.jpf.JPF.main(JPF.java:238) > gov.nasa.jpf.JPFException: class > java.lang.NullPointerException: null > at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1040) > at > gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340) > at > gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84) > at gov.nasa.jpf.JPF.run(JPF.java:308) > at gov.nasa.jpf.JPF.main(JPF.java:238) > > > CONFIGURATION SETTINGS > ====================== > ----------- dictionary contents > branch_start = 1 > d0threshold.class = > gov.nasa.jpf.jvm.DoubleThresholdGenerator > d0threshold.high = 1.0 > d0threshold.low = -1.0 > d0threshold.threshold = 0.0 > jpf.basedir = C:\Temp\jpf_release\bin\.. > jpf.print_exception_stack = true > jpf.version = 3.1.2 > log.level = warning > search.class = gov.nasa.jpf.search.DFSearch > search.error_path = error.xml > search.heuristic.branch.count_early = true > search.heuristic.branch.no_branch_return = -1 > search.heuristic.class = > gov.nasa.jpf.search.heuristic.BFSHeuristic > search.heuristic.comparator.class = > gov.nasa.jpf.search.heuristic.DefaultComparator > search.heuristic.queue_limit = -1 > search.match_depth = false > search.min_free = 1M > search.multiple_errors = false > search.print_errors = true > search.properties = > gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionViolatedProperty:gov.nasa.jpf.jvm > .NoUncaughtExceptionsProperty > vm.atomic_init = true > vm.attributor.class = > gov.nasa.jpf.jvm.DefaultAttributor > vm.bootclasspath = > C:\Temp\jpf_release\bin\../build/env/jpf > vm.check_fp = false > vm.check_fp_compare = true > vm.class = gov.nasa.jpf.jvm.JVM > vm.classpath = build/env/jpf;test > vm.enable_assertions = * > vm.finalize = true > vm.gc = true > vm.halt_on_throw = false > vm.path_output = false > vm.por = true > vm.por.field_boundaries = true > vm.por.fieldlockinfo.class = > gov.nasa.jpf.jvm.StatisticFieldLockInfo > vm.por.sync_detection = true > vm.report.printStacks = true > vm.report.show_bytecode = false > vm.report.show_missing_lines = false > vm.report.show_steps = true > vm.scheduler.class = gov.nasa.jpf.jvm.DefaultScheduler > vm.scheduler.random_seed = 0 > vm.scheduler.use_time_for_seed = false > vm.sourcepath = > C:\Temp\jpf_release\bin\../src:C:\Temp\jpf_release\bin\../examples:C:\Temp\jpf_release\bin\../test > vm.storage.class = gov.nasa.jpf.jvm.Md5StateSet > vm.tree_output = true > vm.verify.ignore_path = true > vm.visible_asserts = false > ----------- free arguments > > Any suggestions on what I may be doing wrong? > > > > __________________________________ > Yahoo! FareChase: Search multiple travel sites in one click. > http://farechase.yahoo.com > > > ------------------------------------------------------- > This SF.Net email is sponsored by the JBoss Inc. Get Certified Today > Register for a JBoss Training Course. Free Certification Exam > for All Training Attendees Through End of 2005. For more info visit: > http://ads.osdn.com/?ad_id=7628&alloc_id=16845&op=click > _______________________________________________ > 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 |
68 messages has been excluded from this view by a project administrator.
