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

[Javapathfinder-user] run-tests build problem ConditionTask "else"

[John M. <jo...@cs...>]

I'm new to javapathfinder. I checked out the main development branch of
the source from the repository with:

$ svn co https://javapathfinder.svn.sourceforge.net/svnroot/javapathfinder javapathfinder/trunk

and then copied the part of this that I gather needs to be installed
to /usr/local/pkg/javapathfinder-20070105 on Slackware Linux 11.0:

$ cd javapathfinder/trunk/trunk
$ cp -R . /usr/local/pkg/javapathfinder-20070105

(I prefer not to clutter up /usr/local itself with installations). I
then ran 'ant run-tests' using ant 1.6.1 and j2sdk 1.5.0_09:

> $ CLASSPATH=/usr/local/pkg/javapathfinder-20070105/lib:/usr/local/pkg/javapathfinder-20070105/build-tools ant run-tests
> Buildfile: build.xml
> 
> init:
>     [mkdir] Created dir: /usr/local/pkg/javapathfinder-20070105/build
>     [mkdir] Created dir: /usr/local/pkg/javapathfinder-20070105/build/jpf
>     [mkdir] Created dir: /usr/local/pkg/javapathfinder-20070105/build/test
>     [mkdir] Created dir: /usr/local/pkg/javapathfinder-20070105/build/env
>     [mkdir] Created dir: /usr/local/pkg/javapathfinder-20070105/build/env/jvm
>     [mkdir] Created dir: /usr/local/pkg/javapathfinder-20070105/build/env/jpf
> 
> BUILD FAILED
> /usr/local/pkg/javapathfinder-20070105/build.xml:124: Class org.apache.tools.ant.taskdefs.ConditionTask doesn't support the "else" attribute.
> 
> Total time: 1 second

Any ideas how to prevent this error?

John A. Murdie
Department of Computer Science
University of York
UK

[Javapathfinder-user] Test gov.nasa.jpf.jvm.TestAssertJPF FAILED

[John M. <jo...@cs...>]

I've just installed javapathfinder-1.0a on Slackware Linux 11 using
J2SDK 1.5.0_09, Ant 1.6.1 and JUnit 3.8.1. All seems well, except that I
see "Test gov.nasa.jpf.jvm.TestAssertJPF FAILED" among the successful
tests of "ant run-tests". The only possibly relevant previous report I
see in the known bugs list or in the mailing list archive is:

http://sourceforge.net/mailarchive/forum.php?thread_id=10220154&forum_id=44903

which suggests that this might not be serious. Is it or is it not? How
can I find out what might have gone wrong?

I append the run-tests part of the "ant run-tests" log. Incidentally, is
the elapsed time of over 5,000 seconds unreasonable on a lightly loaded
Athlon 64 with Slackware Linux 11.0? It was tedious to have to wait for
this to finish, especially as I had no warning that it might take this
long.

John A. Murdie
Department of Computer Science
University of York
UK
-------------------------------------------------------------------------------
run-tests:
     [echo] --- running Junit tests from build/test..
    [junit] Running gov.nasa.jpf.jvm.TestArrayJPF
    [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 2.586
sec
    [junit] Running gov.nasa.jpf.jvm.TestAssertJPF
    [junit] Tests run: 2, Failures: 1, Errors: 0, Time elapsed: 5,039.58
sec
    [junit] Test gov.nasa.jpf.jvm.TestAssertJPF FAILED
    [junit] Running gov.nasa.jpf.jvm.TestCastJPF
    [junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 1.043
sec
    [junit] Running gov.nasa.jpf.jvm.TestExceptionJPF
    [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 2.278
sec
    [junit] Running gov.nasa.jpf.jvm.TestFieldJPF
    [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 1.673
sec
    [junit] Running gov.nasa.jpf.jvm.TestJavaLangClassJPF
    [junit] Tests run: 5, Failures: 0, Errors: 0, Time elapsed: 1.714
sec
    [junit] Running gov.nasa.jpf.jvm.TestMethodJPF
    [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 2.107
sec
    [junit] Running gov.nasa.jpf.jvm.TestNativePeerJPF
    [junit] Tests run: 9, Failures: 0, Errors: 0, Time elapsed: 2.504
sec
    [junit] Running gov.nasa.jpf.jvm.TestThreadJPF
    [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 1.84 sec
    [junit] Running gov.nasa.jpf.jvm.TestWaitJPF
    [junit] Tests run: 3, Failures: 0, Errors: 0, Time elapsed: 1.809
sec
    [junit] Running gov.nasa.jpf.mc.TestCrossingJPF
    [junit] Tests run: 2, Failures: 0, Errors: 0, Time elapsed: 2.218
sec
    [junit] Running gov.nasa.jpf.mc.TestOldClassicJPF
    [junit] Tests run: 2, Failures: 0, Errors: 0, Time elapsed: 1.543
sec
    [junit] Running gov.nasa.jpf.mc.TestRandomJPF
    [junit] Tests run: 2, Failures: 0, Errors: 0, Time elapsed: 1.174
sec
    [junit] Running gov.nasa.jpf.mc.TestVMDeadlockJPF
    [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 2.03 sec

BUILD SUCCESSFUL
Total time: 84 minutes 42 seconds
-------------------------------------------------------------------------------

[Javapathfinder-user] JPF Extension

[Carlos P. <car...@gm...>]

Hi all,

I'm writing an extension to jpf and I would like to ask you a couple of
questions. The point of this extension is to check high-level, abstract,
architectural properties. To achieve this a mapping from patterns of
what I call low-level events (mainly method invocations) to high-level
events (architectural domain events) is defined. Once a high-level event
is emitted -in response to a complete low-level event sequence that was
received from the underlying model checker- a number of actions (that
is, high-level state mutators) would be executed and a number of
assertions (that is, high-level properties that I want to check) would
be proved of the high-level state. Pictorially:

jvm listener
     |
     v
LLEvt1, LLEvt2, ... ---> Mapper---> HLEvt---> Actions (modify HLState)
                                       |
                                       '--> Assertions (check HLState)

(where LL stands for low-level and HL for high-level)

To catch the low-level events I'm listening to executeInstruction events
from the jpf jvm. Upon reception of a low-level event the mapper can
change its internal state (the state of the automata implementing the
patterns). Also eventually a low-level pattern would reach its final
state and a high-level event would be emitted, probably modifying the
high-level state. Both of this state changes are scheduling relevant,
from the point of view of the checker, so every time the mapper state or
the high-level model state change, the current thread should be
rescheduled:

executeInstruction(vm) {
   if instruction is invocation {
     create LLEvent
     feed the mapper with the event
     if mapper.hasChanged or hlState.hasChanged {
        store serialized changed state into jpf system state
        vm.currentThread.reschedule
     }
   }
}

Question #1: is this the right/best way to force a transition?

Notice that I want to store my external states as byte arrays inside jpf own
state. So as a consequence both the mapper and the high-level states
are serializable.
Every time these states change, not only a transition must happen but
also the aforementioned states must be serialized and stored into jpf. I
thought of storing them into jpf's heap area, but I'm not sure at all,
so here goes question #2:

Question #2: is this the right/best way to make jpf aware of external
state?

Well, I think that's all for now. Any help would be appreciated.

Thank you in advance.
Regards,
Carlos

Re: [Javapathfinder-user] info on new abstraction classes

[Peter D. <pe...@cc...>]

here's an answer:

it's an extendable framework for masking and/or transforming what is
considered the state of the program for the purposes of state
matching.  the goal is to reduce the number of states in the state
space without hiding errors.  in many cases, we can spend a little
extra time per state to cut the number of states exponentially.

the "first level" of possible abstractions are activated by using the
gov.nasa.jpf.filter.FilteringSerializer as the vm.serializer.class
(which i believe is the default now).  it uses a "filter
configuration", such as the ...filter.DefaultFilterConfiguration to
determine what fields, etc. should be ignored for state matching.
this FilteringSerializer is rather fast because it generates the
serialized form directly from the VM state and only considers objects
that are reachable from fields and variables that have not been
filtered.  in our DefaultFilterConfiguration, for example, we filter
out lots of unchanging class data that must exist on the heap
according to Java semantics.  in building the serialized form, we also
do full heap canonicalization, meaning references are completely
abstract for the purposes of state matching rather than being tied to
a particular address.

the "second level" of possible abstractions are activated by using the
gov.nasa.jpf.abstraction.AbstractingSerializer.  this option is slower
per state because it constructs an "abstract state graph" that
characterizes the state and serializes that.  this extra step enables
some significant capabilities:

(1) one can write custom "abstractors" for different types of objects.
these "abstractors" can use an arbitrary abstraction function rather
than just one that ignores some of the fields.  the default
"abstractors" use the "filter configuration" for the abstraction,
making this, by default, at least as abstracting as the
FilteringSerializer.

(2) the "abstract state graph" can incorporate abstractions based on
permutational symmetry.  for example, the threads are considered in no
particular order, enabling thread symmetry reduction.  but
permutational symmetry can easily be leveraged elsewhere in the state
without concern for the algorithm that does the reduction.  (this has
been separated out into the StateGraphLinearizer part of the
AbstractingSerializer.)

(3) arbitrary global transformations of the "abstract state graph" can
be plugged in as StateGraphTransforms.


as i have time, i can answer more questions about this work that i did
over the summer as an intern.

and as Willem pointed out, he'll make available some examples of the
abstraction stuff in action.

-- 
Peter Dillinger
pe...@cc...
http://www.peterd.org

Re: [Javapathfinder-user] info on new abstraction classes

[Willem V. <wv...@em...>]

Hi Pavel,

The short answer is no. Hopefully there will be some soon. However you can
check in the examples/ase2006 folder for some examples (read the Readme in
that folder). I'll also soon post the ase2006 tutorial slides that also
contains some info on it.

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 243
 
-----Original Message-----
From: jav...@li...
[mailto:jav...@li...] On Behalf Of
Pavel Parizek
Sent: Friday, December 08, 2006 4:41 AM
To: jav...@li...
Subject: [Javapathfinder-user] info on new abstraction classes

Hello,

I would like to know if there is some documentation for classes in the 
gov/nasa/jpf/jvm/abstraction package, saying what is it good for, how it 
can be used, etc.


Pavel Parizek

-------------------------------------------------------------------------
Take Surveys. Earn Cash. Influence the Future of IT
Join SourceForge.net's Techsay panel and you'll get the chance to share your
opinions on IT & business topics through brief surveys - and earn cash
http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
_______________________________________________
Javapathfinder-user mailing list
Jav...@li...
https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

Re: [Javapathfinder-user] new rudde

[Ernesto R. <sa...@fa...>]

VtAGRA from $ 3. 30 and other goods!

http://www.adesruijnganfeunhandesuin.com
=20
spoken to the school. He left.
As Madam Pomfrey led Harry to a nearby bed, he caught sight of the real
Moody lying motionless in a bed at the far end of the room. His wooden

[Javapathfinder-user] info on new abstraction classes

[Pavel P. <pa...@ne...>]

Hello,

I would like to know if there is some documentation for classes in the 
gov/nasa/jpf/jvm/abstraction package, saying what is it good for, how it 
can be used, etc.


Pavel Parizek

Re: [Javapathfinder-user] presente

[Ath S. <mic...@ga...>]

Hi,

V t a g r a   from $ 3 , 30
http://www.xaseruikingenfunhderunjasderun.com
=20
  _____ =20


Show me.

Re: [Javapathfinder-user] Debugging information from JPF

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

sorry, too consumed with other stuff.

  - 'vm.report.show_threads' prints a stack trace (and lock info) for
    all live threads at the end of a run

  - 'jpf.print_exception_stack' prints a stack trace in case of an  
exception

  - 'vm.halt_on_throw' can be used to stop execution where the exception
    is thrown, i.e. not branch into handlers

The whole reporting needs a thorough overhaul, which is actually one  
of the things we will work on during the next two months.
hope this helps
-- Peter


On Oct 16, 2006, at 2:09 PM, John Penix wrote:
> I think you can get a stack track - maybe there is an option for it?
> At some point the default output was simplified and several things
> were pushed into options.  Some of the best documentation for the
> options is in the default .properties files.

>> I'm using JPF, and it works great, except that the information it  
>> provides
>> is not very helpful in tracking down the root cause of the error.  
>> Is there
>> any way I can get more information when an error is found, a stack  
>> trace for
>> example?

Re: [Javapathfinder-user] Debugging information from JPF

[John P. <jp...@go...>]

Hi Richard,

Since no one is answering...

I think you can get a stack track - maybe there is an option for it?
At some point the default output was simplified and several things
were pushed into options.  Some of the best documentation for the
options is in the default .properties files.

John

On 10/13/06, Markeloff, Richard <Ric...@sp...> wrote:
>
>
>
>
> I'm using JPF, and it works great, except that the information it provides
> is not very helpful in tracking down the root cause of the error. Is there
> any way I can get more information when an error is found, a stack trace for
> example?
>
>
>
> Thanks,
>
>
>
> Rich Markeloff
>
>
>
> ________________________________
>
>
>
> Richard Markeloff
>
> SPARTA, Inc.
>
> 1911 N. Fort Myer Dr., Suite 1100
>
> Arlington, VA 22209
>
>
>
> Voice: 703 647 2414
>
> Fax:    703 558 3410
>
>
> -------------------------------------------------------------------------
> 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
>
>
>


-- 
John Penix
Member of Technical Staff
Google, Inc.

[Javapathfinder-user] Debugging information from JPF

[Markeloff, R. <Ric...@sp...>]

I'm using JPF, and it works great, except that the information it
provides is not very helpful in tracking down the root cause of the
error. Is there any way I can get more information when an error is
found, a stack trace for example?

=20

Thanks,

=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

Re: [Javapathfinder-user] imports from bcel.jar

[Thomas R. <tri...@go...>]

sorry
from README: > 5.2 and not >=5.2

2006/10/11, Thomas Richter <tri...@go...>:
> I have installed bcel5.2.jar and some classes are found - but not all:

[Javapathfinder-user] imports from bcel.jar

[Thomas R. <tri...@go...>]

Hi,
I have installed bcel5.2.jar and some classes are found - but not all:
AnnotationDefault cannot be resolved to a
type	javapathfinder-trunk/src/gov/nasa/jpf/jvm	AnnotationLoader.java	line
438

wkr Thomas

[Javapathfinder-user] native peer for ConcurrentLinkedQueue

[Sergey K. <se...@cs...>]

Hello,

I know this problem has reappeared in the forum/mailing list, however 
after reading through the threads and documentation, I'm still having a 
problem.

I'm checking a program that uses a ConcurrentLinkedQueue. When the object 
is created, it throws this exception:

java.lang.UnsatisfiedLinkError: 
sun.reflect.Reflection.getCallerClass(I)Ljava/lang/Class; (no peer)
         at 
java.util.concurrent.atomic.AtomicReferenceFieldUpdater$AtomicReferenceFieldUpdaterImpl.<init>(AtomicReferenceFieldUpdater.java:152)
         at 
java.util.concurrent.atomic.AtomicReferenceFieldUpdater.newUpdater(AtomicReferenceFieldUpdater.java:64)
         at 
java.util.concurrent.ConcurrentLinkedQueue$Node.<clinit>(ConcurrentLinkedQueue.java:70)
         at 
java.util.concurrent.ConcurrentLinkedQueue.<init>(ConcurrentLinkedQueue.java:133)
         at EditorThread.<init>(EditorThread.java:302)
         at ConcurrentEditor.main(ConcurrentEditor.java:41)


I 'solved' the problem by writing a peer class for the queue in 
env/jvm. Here's shortened version of the class:


 	package gov.nasa.jpf.jvm;

 	import java.util.concurrent.ConcurrentLinkedQueue;
 	import java.util.HashMap;

 	static HashMap<Integer,ConcurrentLinkedQueue<Integer>> queues =
 	    new HashMap<Integer,ConcurrentLinkedQueue<Integer>>();

 	public static void $init____V (MJIEnv env, int objref) {
     	  ConcurrentLinkedQueue<Integer> q = new
 		ConcurrentLinkedQueue<Integer>();
 	  queues.put(objref, q);
 	}

 	public static boolean offer__Ljava_lang_Object_2__Z (MJIEnv env,
 		int robj, int rObject0) {
 	  return queues.get(robj).offer(rObject0);
 	}

 	public static int poll____Ljava_lang_Object_2 (MJIEnv env, int robj) {
 	  return queues.get(robj).poll();
 	}

I simply created the native queue and maintained a HashMap of the queues
(following the example in DecimalFormat). For the offer and poll operations
I simply enqueued and dequeued the int values (representing the objects)
that were passed as parameters.

But the problem came when the 'poll' operation had to return the 
reference of the enqueued object.

It returns a correct reference, BUT unfortunately, the garbage collector
already removed the previously enqueued object from the dynamic heap.

So in the end I get a NullPointerException in CHECKCAST method, line 53 
because on line 51, 'e' becomes 'null' (as the object doesn't exist on the 
heap).

So my question is, am I correctly writing the native peer class (it 
actually works very well on small programs, but not on large ones). If 
not, is there any other way of solving this problem apart from writing the 
model class?

I hope I explained the problem correctly.
Thanks very much
sergey

[Javapathfinder-user] Turning off POR

[Markeloff, R. <Ric...@sp...>]

As an experiment, I've tried turning off POR by setting vm.por =3D false
in default.properties. The resulting stack trace is shown below. Is
running without POR still a supported option?

Thanks,

Rich Markeloff


Java Pathfinder Model Checker v4.0a - (C) 1999-2006 RIACS/NASA Ames
Research Center
JPF exception, terminating: class gov.nasa.jpf.JPFException: class
java.lang.NullPointerException: null
java.lang.NullPointerException
	at
gov.nasa.jpf.jvm.bytecode.FieldInstruction.isLockProtected(FieldInstruct
ion.java:120)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isSchedulingRelevant(St
aticFieldInstruction.java:63)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isNewPorFieldBoundary(S
taticFieldInstruction.java:42)
	at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:45)
	at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1475)
	at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1974)
	at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:433)
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1190)
	at gov.nasa.jpf.search.Search.forward(Search.java:337)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
	at gov.nasa.jpf.JPF.run(JPF.java:328)
	at gov.nasa.jpf.JPF.main(JPF.java:259)
java.lang.NullPointerException
	at
gov.nasa.jpf.jvm.bytecode.FieldInstruction.isLockProtected(FieldInstruct
ion.java:120)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isSchedulingRelevant(St
aticFieldInstruction.java:63)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isNewPorFieldBoundary(S
taticFieldInstruction.java:42)
	at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:45)
	at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1475)
	at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1974)
	at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:433)
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1190)
	at gov.nasa.jpf.search.Search.forward(Search.java:337)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
	at gov.nasa.jpf.JPF.run(JPF.java:328)
	at gov.nasa.jpf.JPF.main(JPF.java:259)
gov.nasa.jpf.JPFException: class java.lang.NullPointerException: null
	at
gov.nasa.jpf.jvm.bytecode.FieldInstruction.isLockProtected(FieldInstruct
ion.java:122)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isSchedulingRelevant(St
aticFieldInstruction.java:63)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isNewPorFieldBoundary(S
taticFieldInstruction.java:42)
	at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:45)
	at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1475)
	at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1974)
	at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:433)
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1190)
	at gov.nasa.jpf.search.Search.forward(Search.java:337)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
	at gov.nasa.jpf.JPF.run(JPF.java:328)
	at gov.nasa.jpf.JPF.main(JPF.java:259)
java.lang.NullPointerException
	at
gov.nasa.jpf.jvm.bytecode.FieldInstruction.isLockProtected(FieldInstruct
ion.java:120)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isSchedulingRelevant(St
aticFieldInstruction.java:63)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isNewPorFieldBoundary(S
taticFieldInstruction.java:42)
	at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:45)
	at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1475)
	at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1974)
	at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:433)
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1190)
	at gov.nasa.jpf.search.Search.forward(Search.java:337)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
	at gov.nasa.jpf.JPF.run(JPF.java:328)
	at gov.nasa.jpf.JPF.main(JPF.java:259)
gov.nasa.jpf.JPFException: class java.lang.NullPointerException: null
	at
gov.nasa.jpf.jvm.bytecode.FieldInstruction.isLockProtected(FieldInstruct
ion.java:122)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isSchedulingRelevant(St
aticFieldInstruction.java:63)
	at
gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction.isNewPorFieldBoundary(S
taticFieldInstruction.java:42)
	at
gov.nasa.jpf.jvm.bytecode.GETSTATIC.execute(GETSTATIC.java:45)
	at
gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1475)
	at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1974)
	at
gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:433)
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1190)
	at gov.nasa.jpf.search.Search.forward(Search.java:337)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
	at gov.nasa.jpf.JPF.run(JPF.java:328)
	at gov.nasa.jpf.JPF.main(JPF.java:259)
gov.nasa.jpf.JPFException: class gov.nasa.jpf.JPFException: class
java.lang.NullPointerException: null
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1228)
	at gov.nasa.jpf.search.Search.forward(Search.java:337)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
	at gov.nasa.jpf.JPF.run(JPF.java:328)
	at gov.nasa.jpf.JPF.main(JPF.java:259)

                                                          =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

Re: [Javapathfinder-user] PHAmrhRMACY

[Ine R. <cra...@fo...>]

Hi
=20
All you l r PH m ARM x AC i Y d n ire y ctl x y from the ma s nuf c act
o ur d er,
Your ch q anc y e to e c cono b miz s e up t o o 50 o % wit h h
http://www.zkonmdetindaseun.com

Re: [Javapathfinder-user] PHAwjRMACY

[Larkin S. <van...@ke...>]

Hi
=20
All you x r P g HAR e MAC n Y dir u ect g ly from the man f ufac r tur a
er,
Your ch a an x ce to ec q onom p ize wit o h us
http://www.yahufasedunkades.com

Re: [Javapathfinder-user] PHfAtRMA

[Sachie H. <gru...@ho...>]

Hi

VAngLIUM

VIcmAGRA

CIzjALIS

AMpdBIEN

http://buyaderunjawuin.com

Re: [Javapathfinder-user] 'length' operation on cloned arrays produces JPF exception

[Peter D. <pe...@cc...>]

Object.clone() should now be fully functional.  do an SVN update to
get the latest version.

-- 
Peter Dillinger
pe...@cc...
http://www.peterd.org

Re: [Javapathfinder-user] 'length' operation on cloned arrays produces JPF exception

[Peter D. <pe...@cc...>]

this can be considered a "known limitation", by looking at the
relevant source code in env/jvm/gov.nasa.jpf.jvm.JPF_java_lang_Object:


  public static int clone____Ljava_lang_Object_2 (MJIEnv env, int
objref) {
    // <2do>
    return -1;
  }


the -1 here means that Object.clone() is always going to return null.
one of us should implement this, and it probably wouldn't be very
hard.  i'll work on it for a little while and post another reply if i
fix it.

-peter d

On Tue, Sep 05, 2006 at 02:48:06PM -0400, Sergey Kulikov wrote:
> 
> Hi, I'm not sure if it's a bug, but the following code produces a JPF 
> nullpointer exception at ARRAYLENGTH.java: 39. Basically the objref is -1 
> after th.pop() operation.
> 
>      int[] a = new int[3];
>      int[] b = (int[])a.clone();
>      int c = b.length;
> 
> This seems to occur when you call a 'length' operation on a cloned array.
> 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

-- 
Peter Dillinger
pe...@cc...
http://www.peterd.org

[Javapathfinder-user] 'length' operation on cloned arrays produces JPF exception

[Sergey K. <se...@cs...>]

Hi, I'm not sure if it's a bug, but the following code produces a JPF 
nullpointer exception at ARRAYLENGTH.java: 39. Basically the objref is -1 
after th.pop() operation.

     int[] a = new int[3];
     int[] b = (int[])a.clone();
     int c = b.length;

This seems to occur when you call a 'length' operation on a cloned array.
thanks
sergey

Re: [Javapathfinder-user] I can't build Java PathFinder

[<lei...@gm...>]

Hi,

Thank you very much for your quick reply, Now, I have solved the problem,
the cause is that I added the ant.jar and junit-4.1.jar to the CLASSPATH,
and this brought exception NoClassDefFoundError exception occurred when I
ran the command "java RunAnt run-tests".

Thanks again!

Lei Wang


2006/9/4, Peter Dillinger <pe...@cc...>:
>
> it looks like you should change directory to F:\JPF4\trunk before
> running RunAnt:
>
>        cd F:\JPF4\trunk
>        java RunAnt run-tests
>
> i'm assuming F:\JPF4\trunk is the directory containing files like
> "build.xml", "default.properties" and "RunAnt.class".
>
> where did the directory org\apache\tools... come from?  it's not in
> the SVN repository.
>
> keep in mind you don't need to install Ant yourself or unpack any JAR
> files to build and execute JPF.
>
> -peter d
>
> On Mon, Sep 04, 2006 at 09:32:25PM +0800, ???? wrote:
> > Hi everyone,
> >
> > I have retrieved the files from the repository successfully, however,
> I'm
> > having trouble building JPF. When I compiled the whole system using
> command
> > line "java RunAnt run-tests" as
> > the manual says, exception occurred with the message :
> >
> > F:\JPF4\trunk\org\apache\tools\ant\launch\AntMain>java RunAnt run-tests
> > Exception in thread "main" java.lang.RuntimeException: Unable to find
> JPF
> > home dir.  Either make current directory, or put in classpath.
> >        at RunAnt.computeJpfHome(RunAnt.java:153)
> >        at RunAnt.main(RunAnt.java:329)
> >
> > It seemed that the JPF home directory cannot be found, has anyone seen
> this
> > problem before?
> >
> > Many thanks!
> >
> > Lei Wang
> >
> > ----------
> > Software Engineering Institute
> > Xidian University
> > Xi'an,China
>
> >
> -------------------------------------------------------------------------
> > 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
>
>
> --
> Peter Dillinger
> pe...@cc...
> http://www.peterd.org
>

Re: [Javapathfinder-user] I can't build Java PathFinder

[Peter D. <pe...@cc...>]

it looks like you should change directory to F:\JPF4\trunk before
running RunAnt:

	cd F:\JPF4\trunk
	java RunAnt run-tests

i'm assuming F:\JPF4\trunk is the directory containing files like
"build.xml", "default.properties" and "RunAnt.class".

where did the directory org\apache\tools... come from?  it's not in
the SVN repository.

keep in mind you don't need to install Ant yourself or unpack any JAR
files to build and execute JPF.

-peter d

On Mon, Sep 04, 2006 at 09:32:25PM +0800, ???? wrote:
> Hi everyone,
> 
> I have retrieved the files from the repository successfully, however, I'm
> having trouble building JPF. When I compiled the whole system using command
> line "java RunAnt run-tests" as
> the manual says, exception occurred with the message :
> 
> F:\JPF4\trunk\org\apache\tools\ant\launch\AntMain>java RunAnt run-tests
> Exception in thread "main" java.lang.RuntimeException: Unable to find JPF
> home dir.  Either make current directory, or put in classpath.
>        at RunAnt.computeJpfHome(RunAnt.java:153)
>        at RunAnt.main(RunAnt.java:329)
> 
> It seemed that the JPF home directory cannot be found, has anyone seen this
> problem before?
> 
> Many thanks!
> 
> Lei Wang
> 
> ----------
> Software Engineering Institute
> Xidian University
> Xi'an,China

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


-- 
Peter Dillinger
pe...@cc...
http://www.peterd.org

[Javapathfinder-user] I can't build Java PathFinder

[<lei...@gm...>]

Hi everyone,

I have retrieved the files from the repository successfully, however, I'm
having trouble building JPF. When I compiled the whole system using command
line "java RunAnt run-tests" as
the manual says, exception occurred with the message :

F:\JPF4\trunk\org\apache\tools\ant\launch\AntMain>java RunAnt run-tests
Exception in thread "main" java.lang.RuntimeException: Unable to find JPF
home dir.  Either make current directory, or put in classpath.
        at RunAnt.computeJpfHome(RunAnt.java:153)
        at RunAnt.main(RunAnt.java:329)

It seemed that the JPF home directory cannot be found, has anyone seen this
problem before?

Many thanks!

Lei Wang

----------
Software Engineering Institute
Xidian University
Xi'an,China

Re: [Javapathfinder-user] Getting started with JPF4

[Peter D. <pe...@cc...>]

On Fri, Sep 01, 2006 at 12:42:32PM -0400, Markeloff, Richard wrote:
> 1) Numerous build errors in examples/issta2006 and
> test/gov/nasa/jpf/peterd_tests. I just deleted these packages from the
> project.

make sure your Java Compiler settings are at least 5.0, with support
for Annotations, Generics, etc.

also, be sure your build path is configured properly.  if you created
the project without going through the SVN Checkout wizard and checking
out "trunk", you might not have the correct build path.  (by the way,
the "build path" is in a file called .classpath, which is in /trunk of
the repository:

<?xml version="1.0" encoding="UTF-8"?>
<classpath>
        <classpathentry kind="src" path="src"/>
        <classpathentry kind="src" path="extensions/overflow/src"/>
        <classpathentry output="build/env/jpf" kind="src" path="extensions/ui/env/jpf"/>
        <classpathentry output="build/env/jvm" kind="src" path="extensions/ui/env/jvm"/>
        <classpathentry kind="src" path="extensions/ui/src"/>
        <classpathentry output="build/examples" kind="src" path="examples"/>
        <classpathentry output="build/test" kind="src" path="test"/>
        <classpathentry output="build/env/jpf" kind="src" path="env/jpf"/>
        <classpathentry output="build/env/jvm" kind="src" path="env/jvm"/>
        <classpathentry output="build-tools/noshell/build" kind="src" path="build-tools/noshell/src"/>
        <classpathentry kind="src" path="extensions/abstraction/src"/>
        <classpathentry kind="src" path="extensions/LTL2Buchi/src"/>
        <classpathentry kind="src" path="extensions/symbolic/src"/>
        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
        <classpathentry kind="lib" path="lib/bcel.jar"/>
        <classpathentry kind="lib" path="build-tools/lib/junit-4.1.jar"/>
        <classpathentry kind="lib" path="extensions/symbolic/lib/cream.jar"/>
        <classpathentry kind="lib" path="extensions/symbolic/lib/de.jar"/>
        <classpathentry kind="lib" path="extensions/symbolic/lib/solver.jar"/>
        <classpathentry kind="output" path="build/jpf"/>
</classpath>


> 2) When I attempt to run the Deadlock example, I get the following:
> 
>  
> 
> JPF configuration error: class not found
> gov.nasa.jpf.filter.FilteringSerializer
> 
> > used within "vm.class" instantiation of class gov.nasa.jpf.jvm.JVM
> 
>  
> 
> I don't see any gov.nasa.jpf.filter package in the distribution. Where
> could it be?

extensions/abstraction/src, which is in the distributed build path
(and Ant build.xml)

-- 
Peter Dillinger
pe...@cc...
http://www.peterd.org