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

[Javapathfinder-user] java.lang.UnsatisfiedLinkError (no peer)

[Shane D. <sha...@ho...>]

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?

Re: [Javapathfinder-user] loop example

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

try printing out n before you go into the loop.  parseInt  and readLine
might not be properly implemented in JPF.  if n=3D0 that could be the probl=
em.

John

On 4/10/06, Arkadeb Ghosal <ar...@gm...> wrote:
>
> Hi,
>
>  when i am verifying a loop with a constant there is no problem while for
> the following example, JPF reports stack out of bound exception ...
> the example comilation doesn't report any error ...
> any suggestions ?
>
> class HelloWorld {
>   public static void main (String[] args) throws IOException {
>     System.out.println("Hello World!");
>
>     int sum =3D 0;
>     BufferedReader in =3D new BufferedReader(new InputStreamReader(
> System.in <http://www.google.com/url?sa=3DD&q=3Dhttp%3A%2F%2FSystem.in>))=
;
>     int n =3D Integer.parseInt(in.readLine());
>
>     for (int i =3D 1; i <=3D n; i++)
>         sum =3D sum + i;
>
>     int tot =3D n*(n+1) / 2;
>
>     assert (sum =3D=3D tot);
>   }
> }
>

[Javapathfinder-user] loop example

[Arkadeb G. <ar...@gm...>]

Hi,

 when i am verifying a loop with a constant there is no problem while for
the following example, JPF reports stack out of bound exception ...
the example comilation doesn't report any error ...
any suggestions ?

class HelloWorld {
  public static void main (String[] args) throws IOException {
    System.out.println("Hello World!");

    int sum =3D 0;
    BufferedReader in =3D new BufferedReader(new InputStreamReader(System.i=
n
));
    int n =3D Integer.parseInt(in.readLine());

    for (int i =3D 1; i <=3D n; i++)
        sum =3D sum + i;

    int tot =3D n*(n+1) / 2;

    assert (sum =3D=3D tot);
  }
}

RE: [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #59 - 2 msgs

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

Hi Arko,
 
First thing: NEVER change default.properties! You can change
jpf.properties if you like, but not defaults. I suggest downloading the
old version from CVS to fix things.
 
Your problem is that the vmbootclasspath is not set to pick up the
classes where JPF overrides some java library classes. Basically put in
the line you use to have there to point tobuild/env/jpf.
 
If you don't want to fudge with the properties just add the
build/env/jpf and build/env/jvm folders to your classpath in Eclipse's
run-script for running JPF on your example.
 
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
Arkadeb Ghosal
Sent: Monday, April 10, 2006 2:13 PM
To: wv...@em...
Cc: jav...@li...
Subject: Re: [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1
#59 - 2 msgs
 
Hi Willem,

 I ran ant-build which reported "successful". The build/env/jpf
directory is also being built. However the execution is not going
through (the error changed which implies something has improved). 

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\Unkown:0) 

the following lines in default.properties were modified:

jpf.basedir = .
vm.bootclasspath = ${jpf.basedir}/build/env/jpf
vm.classpath = build/examples

to 
jpf.basedir= C:\\Documents\ and\ Settings\\arkadeb\\My\
Documents\\Eclipse\ Workspace\ Projects\\JPF
vm.classpath  = ${jpf.basedir}/examples

any suggestions how to remove the error ? 

Thanks a lot for your help 
- arko
On 4/10/06, Willem Visser <wv...@em...> wrote: 
Hi Arko,
 
If there is no build/env/jpf directory it sounds like the compilation
didn't happen. Right click on the build.xml file and run ant on it. 
 
I use Eclipse with JPF and quite frankly it is best to compile the thing
with ant (even if you have to do it outside Eclipse). Of course I change
JPF a lot and hence I need to compile it often so I spent some time
setting it up to be directly compiling in Eclipse. 
 
Once it is compiled correctly running it should be trivial if you follow
the steps Eric suggested. Let us know if you still have trouble.
 
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
Arkadeb Ghosal
Sent: Sunday, April 09, 2006 10:41 PM
To: jav...@li...
Subject: [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #59
- 2 msgs
 
Hi Eric,

 Thanks a lot for the advice but i am still getting the same error. 

jpf.basedir = .
vm.bootclasspath = ${jpf.basedir}/build/env/jpf
vm.classpath = build/examples

my windows directory is 
C:\Documents and Settings\arkadeb\My Documents\Eclipse Workspace
Projects\JPF

so replaced 
jpf.basedir= C:\\Documents\ and\ Settings\\arkadeb\\My\
Documents\\Eclipse\ Workspace\ Projects\\JPF
.. it gave the same error ... 

also there is no build/env/jpf in the directory ...
there are env/jpf under the main project directory 

any help would be great ...

Thanks again
arko
 

Re: [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #59 - 2 msgs

[Arkadeb G. <ar...@gm...>]

Hi Willem,

 I ran ant-build which reported "successful". The build/env/jpf directory i=
s
also being built. However the execution is not going through (the error
changed which implies something has improved).

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\Unkown:0)

the following lines in default.properties were modified:

jpf.basedir =3D .
vm.bootclasspath =3D ${jpf.basedir}/build/env/jpf
vm.classpath =3D build/examples

to
jpf.basedir=3D C:\\Documents\ and\ Settings\\arkadeb\\My\ Documents\\Eclips=
e\
Workspace\ Projects\\JPF
vm.classpath  =3D ${jpf.basedir}/examples

any suggestions how to remove the error ?

Thanks a lot for your help
- arko

On 4/10/06, Willem Visser <wv...@em...> wrote:
>
>  Hi Arko,
>
>
>
> If there is no build/env/jpf directory it sounds like the compilation
> didn't happen. Right click on the build.xml file and run ant on it.
>
>
>
> I use Eclipse with JPF and quite frankly it is best to compile the thing
> with ant (even if you have to do it outside Eclipse). Of course I change =
JPF
> a lot and hence I need to compile it often so I spent some time setting i=
t
> up to be directly compiling in Eclipse.
>
>
>
> Once it is compiled correctly running it should be trivial if you follow
> the steps Eric suggested. Let us know if you still have trouble.
>
>
>
> 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 *Arkadeb
> Ghosal
> *Sent:* Sunday, April 09, 2006 10:41 PM
> *To:* jav...@li...
> *Subject:* [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #5=
9
> - 2 msgs
>
>
>
> Hi Eric,
>
>  Thanks a lot for the advice but i am still getting the same error.
>
> jpf.basedir =3D .
> vm.bootclasspath =3D ${jpf.basedir}/build/env/jpf
> vm.classpath =3D build/examples
>
> my windows directory is
> C:\Documents and Settings\arkadeb\My Documents\Eclipse Workspace
> Projects\JPF
>
> so replaced
> jpf.basedir=3D C:\\Documents\ and\ Settings\\arkadeb\\My\
> Documents\\Eclipse\ Workspace\ Projects\\JPF
> .. it gave the same error ...
>
> also there is no build/env/jpf in the directory ...
> there are env/jpf under the main project directory
>
> any help would be great ...
>
> Thanks again
> arko
>

RE: [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #59 - 2 msgs

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

Hi Arko,
 
If there is no build/env/jpf directory it sounds like the compilation
didn't happen. Right click on the build.xml file and run ant on it. 
 
I use Eclipse with JPF and quite frankly it is best to compile the thing
with ant (even if you have to do it outside Eclipse). Of course I change
JPF a lot and hence I need to compile it often so I spent some time
setting it up to be directly compiling in Eclipse. 
 
Once it is compiled correctly running it should be trivial if you follow
the steps Eric suggested. Let us know if you still have trouble.
 
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
Arkadeb Ghosal
Sent: Sunday, April 09, 2006 10:41 PM
To: jav...@li...
Subject: [Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #59
- 2 msgs
 
Hi Eric,

 Thanks a lot for the advice but i am still getting the same error. 

jpf.basedir = .
vm.bootclasspath = ${jpf.basedir}/build/env/jpf
vm.classpath = build/examples

my windows directory is 
C:\Documents and Settings\arkadeb\My Documents\Eclipse Workspace
Projects\JPF

so replaced 
jpf.basedir= C:\\Documents\ and\ Settings\\arkadeb\\My\
Documents\\Eclipse\ Workspace\ Projects\\JPF
.. it gave the same error ... 

also there is no build/env/jpf in the directory ...
there are env/jpf under the main project directory 

any help would be great ...

Thanks again
arko

[Javapathfinder-user] Re: Javapathfinder-user digest, Vol 1 #59 - 2 msgs

[Arkadeb G. <ar...@gm...>]

Hi Eric,

 Thanks a lot for the advice but i am still getting the same error.

jpf.basedir =3D .
vm.bootclasspath =3D ${jpf.basedir}/build/env/jpf
vm.classpath =3D build/examples

my windows directory is
C:\Documents and Settings\arkadeb\My Documents\Eclipse Workspace
Projects\JPF

so replaced
jpf.basedir=3D C:\\Documents\ and\ Settings\\arkadeb\\My\ Documents\\Eclips=
e\
Workspace\ Projects\\JPF
.. it gave the same error ...

also there is no build/env/jpf in the directory ...
there are env/jpf under the main project directory

any help would be great ...

Thanks again
arko

Re: [Javapathfinder-user] JPF and Eclipse

[Eric P. <pl...@ni...>]

Hi Arkadeb,

It seems you have a path problem. JPF needs you to setup the 
jpf.basedir, vm.classpath, and vm.bootclasspath in the property file (or 
directly on the command line with +attrib=value). In the trace you sent 
in the message, you have the default values and it may not point to your 
installation directories. You may customize jpf.properties or create 
your own (remeber to call JPF with the -c option then) to point to the 
right directories.

Note that:
- When you use the command line +attrib=value, you may encounter a 
problem depending on your version of JPF. The spaces around the `=' mark 
can be the problem and you can try to remove them. Peter from the JPF 
team fixed this several months ago though.
- If you are under Windows, the paths require to escape the backslash. 
If you install in c:\myFolder, you probably need to write in the config 
file/command line: c:\\myFolder. If your path contains space, they 
should be escaped as well.

I hope this might help you.

Eric



Arkadeb Ghosal wrote:
> Hi,
>
>  I am new to JPF and tried to install it in Eclipse.
> The build was successful (only 10 warnings).
>
> I tried to run it with the following options:
>
> main file: gov.nasa.jpf.JPF
> arguments: -show examples/HelloWorld
> JPF has been included in the classpath ...
>
> however it does not run properly: an error is generated as follows:
> error during VM runtime initialization: wrong model classes (check 
> vm.[boot]classpath)
>
> the full error trace is posted below.
>
> any suggestions would be highly appreciated.
>
> Thanks
> arko
>
> ----------- 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 = .
> 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 = ./build/env/jpf
> vm.check_fp = false
> vm.check_fp_compare = true
> vm.class = gov.nasa.jpf.jvm.JVM
> vm.classpath = build/examples
> 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 = ./src:./examples:./test
> vm.storage.class = gov.nasa.jpf.jvm.Md5StateSet
> vm.tree_output = true
> vm.verify.ignore_path = true
> vm.visible_asserts = false
> ----------- free arguments
> -show
> examples/HelloWorld
> error during VM runtime initialization: wrong model classes (check 
> vm.[boot]classpath)

[Javapathfinder-user] JPF and Eclipse

[Arkadeb G. <ar...@gm...>]

Hi,

 I am new to JPF and tried to install it in Eclipse.
The build was successful (only 10 warnings).

I tried to run it with the following options:

main file: gov.nasa.jpf.JPF
arguments: -show examples/HelloWorld
JPF has been included in the classpath ...

however it does not run properly: an error is generated as follows:
error during VM runtime initialization: wrong model classes (check
vm.[boot]classpath)

the full error trace is posted below.

any suggestions would be highly appreciated.

Thanks
arko

----------- dictionary contents
branch_start =3D 1
d0threshold.class =3D gov.nasa.jpf.jvm.DoubleThresholdGenerator
d0threshold.high =3D 1.0
d0threshold.low =3D -1.0
d0threshold.threshold =3D 0.0
jpf.basedir =3D .
jpf.print_exception_stack =3D true
jpf.version =3D 3.1.2
log.level =3D warning
search.class =3D gov.nasa.jpf.search.DFSearch
search.error_path =3D error.xml
search.heuristic.branch.count_early =3D true
search.heuristic.branch.no_branch_return =3D -1
search.heuristic.class =3D gov.nasa.jpf.search.heuristic.BFSHeuristic
search.heuristic.comparator.class =3D
gov.nasa.jpf.search.heuristic.DefaultComparator
search.heuristic.queue_limit =3D -1
search.match_depth =3D false
search.min_free =3D 1M
search.multiple_errors =3D false
search.print_errors =3D true
search.properties =3D
gov.nasa.jpf.jvm.NotDeadlockedProperty:gov.nasa.jpf.jvm.NoAssertionViolated=
Property:gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
vm.atomic_init =3D true
vm.attributor.class =3D gov.nasa.jpf.jvm.DefaultAttributor
vm.bootclasspath =3D ./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
vm.enable_assertions =3D *
vm.finalize =3D true
vm.gc =3D true
vm.halt_on_throw =3D false
vm.path_output =3D false
vm.por =3D true
vm.por.field_boundaries =3D true
vm.por.fieldlockinfo.class =3D gov.nasa.jpf.jvm.StatisticFieldLockInfo
vm.por.sync_detection =3D true
vm.report.printStacks =3D true
vm.report.show_bytecode =3D false
vm.report.show_missing_lines =3D false
vm.report.show_steps =3D true
vm.scheduler.class =3D gov.nasa.jpf.jvm.DefaultScheduler
vm.scheduler.random_seed =3D 0
vm.scheduler.use_time_for_seed =3D false
vm.sourcepath =3D ./src:./examples:./test
vm.storage.class =3D gov.nasa.jpf.jvm.Md5StateSet
vm.tree_output =3D true
vm.verify.ignore_path =3D true
vm.visible_asserts =3D false
----------- free arguments
-show
examples/HelloWorld
error during VM runtime initialization: wrong model classes (check
vm.[boot]classpath)

[Javapathfinder-user] can we stop JPF in the middle

[zuo j. <zu...@pk...>]

I want to know if we can stop JPF execution in our program before all the
scenarios are enumerated. This is useful to split a large number of
scenarios into several chunks and do analysis on a chunk each time. Thanks!

 

J. H. Zuo

RE: [Javapathfinder-user] RE: Using Heuristics in JPF

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

Hi Ali,
 
We have had a hectic day so have not had a chance to respond to your
issue yet.
 
Basically we had a bug that made the heuristics that don't conform to
(Config,Search) signature to fail. That is now fixed, and it now also
accepts (Config) by itself. However some of the heuristics still only
have (Search) as well and that is wrong - and need to be fixed in
exactly the fashion you did by adding the config.
 
Thanks for reporting the bug!
 
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
Ali Taleghani
Sent: Monday, March 27, 2006 5:21 PM
To: jav...@li...
Subject: [Javapathfinder-user] RE: Using Heuristics in JPF
 
Hi,
As a continuation to the problem below, I noticed that the constructors
of BFSHeuristic, GlobalBranchCoverage and ChooseFree have the following
signatures:
 
public BFSHeuristic (Config config, HeuristicSearch hSearch)
 
public ChooseFree (HeuristicSearch hSearch)
 
public GlobalBranchCoverage (Config config)
 
 
Once I changed all to 

public HeuristicName (Config config, HeuristicSearch hSearch)
 
the problem listed below disappeared. Is it possible that the signatures
of the Heuristics classes are not correct?
 
Thank you

Ali
 
-----Original Message-----
From: Ali Taleghani [mailto:ata...@cs...] 
Sent: Monday, March 27, 2006 12:42 PM
To: 'jav...@li...'
Subject: Using Heuristics in JPF
 
Hi,
I am trying to use the Heuristic classes in JPF. Is there a restriction
of which Heuristic class can be used with which Heuristic search?
From all the Heuristics, I can only make "BFSHeuristic" work. For any
other Heuristic that I use either with HeuristicSearch or BeamSearch I
get the following error:
 
JPF configuration error: error instantiating class
gov.nasa.jpf.search.heuristic.GlobalBranchCoverage for entry 
"search.heuristic.class":no suitable ctor found
>used within "search.class" instantiation of class
gov.nasa.jpf.search.heuristic.HeuristicSearch
 
I would appreciate any help.
 
Thank you
 
Ali Taleghani
University of Waterloo

[Javapathfinder-user] RE: Using Heuristics in JPF

[Ali T. <ata...@cs...>]

Hi,
As a continuation to the problem below, I noticed that the constructors
of BFSHeuristic, GlobalBranchCoverage and ChooseFree have the following
signatures:
 
public BFSHeuristic (Config config, HeuristicSearch hSearch)
 
public ChooseFree (HeuristicSearch hSearch)
 
public GlobalBranchCoverage (Config config)
 
 
Once I changed all to 

public HeuristicName (Config config, HeuristicSearch hSearch)
 
the problem listed below disappeared. Is it possible that the signatures
of the Heuristics classes are not correct?
 
Thank you

Ali
 
-----Original Message-----
From: Ali Taleghani [mailto:ata...@cs...] 
Sent: Monday, March 27, 2006 12:42 PM
To: 'jav...@li...'
Subject: Using Heuristics in JPF
 
Hi,
I am trying to use the Heuristic classes in JPF. Is there a restriction
of which Heuristic class can be used with which Heuristic search?
From all the Heuristics, I can only make "BFSHeuristic" work. For any
other Heuristic that I use either with HeuristicSearch or BeamSearch I
get the following error:
 
JPF configuration error: error instantiating class
gov.nasa.jpf.search.heuristic.GlobalBranchCoverage for entry 
"search.heuristic.class":no suitable ctor found
>used within "search.class" instantiation of class
gov.nasa.jpf.search.heuristic.HeuristicSearch
 
I would appreciate any help.
 
Thank you
 
Ali Taleghani
University of Waterloo

[Javapathfinder-user] Using Heuristics in JPF

[Ali T. <ata...@cs...>]

Hi,
I am trying to use the Heuristic classes in JPF. Is there a restriction
of which Heuristic class can be used with which Heuristic search?
From all the Heuristics, I can only make "BFSHeuristic" work. For any
other Heuristic that I use either with HeuristicSearch or BeamSearch I
get the following error:
 
JPF configuration error: error instantiating class
gov.nasa.jpf.search.heuristic.GlobalBranchCoverage for entry 
"search.heuristic.class":no suitable ctor found
>used within "search.class" instantiation of class
gov.nasa.jpf.search.heuristic.HeuristicSearch
 
I would appreciate any help.
 
Thank you
 
Ali Taleghani
University of Waterloo

Re: [Javapathfinder-user] contracts in javapathfinder

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

We don't support JML directly, but you can put assertions into the
code at the appropriate places.

John

On 3/15/06, harry huang <har...@ho...> wrote:
> Hi,
>
> I have a question how to write the precondtion, postcondition and class
> invariant in the java pathfinder. Can we write the code semantics(
> precondtion, postcondition and class invariant )  like JML in java
> pathfinder ?
>
> harry
>
>
>
>
> -------------------------------------------------------
> This SF.Net email is sponsored by xPML, a groundbreaking scripting langua=
ge
> that extends applications into web and mobile media. Attend the live webc=
ast
> and join the prime developer group breaking into this new coding territor=
y!
> http://sel.as-us.falkag.net/sel?cmd=3Dlnk&kid=3D110944&bid=3D241720&dat=
=3D121642
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

[Javapathfinder-user] report on two NullPointer Exceptions

[zuo j. <zu...@pk...>]

Hi, during my use with JPF, I found two cases of NullPointer Exception
reported by JPF.

Case 1:

 java.lang.NullPointerException

        at =
gov.nasa.jpf.jvm.DynamicArea.markRecursive(DynamicArea.java:310)

        at =
gov.nasa.jpf.jvm.DynamicArea.analyzeHeap(DynamicArea.java:161)

       =A1=AD

Reason:

    At line 161 in DynamicArea.analyzeHeap(), elements[i] may be null. =
And
in markRecursive() there is no guard to test if the parameter is null.
Hence, a guard is needed to ensure elements[i] passed to markRecursive() =
is
not null.

=20

  Case 2:

     java.lang.NullPointerException

                   at
gov.nasa.jpf.jvm.bytecode.INVOKESPECIAL.isSchedulingRelevant(INVOKESPECIA=
L.j
ava: 81)

                   =A1=AD

   Reason:=20

         In INVOKESPECIAL.isSchedulingRelevant(), there is a statement:

MethodInfo mi =3D getInvokedMethod( ti, ks);

In fact, mi may be null. Hence, a guard is needed to ensure the =
reference to
mi is valid.

=20

J. H. Zuo

[Javapathfinder-user] byte to char fails

[zuo j. <zu...@pk...>]

Thank your advice! I considered moving the implementation of parsing =
into a
peer method. But several reasons prohibited me to do so. The main reason =
is
that the Rule objects constructed out of parsing have to interact with =
the
module running in JPF in complex manner. So, I decide to try
RandomAccessFile. When I use RandomAccessFile.read(byte[] data, =A1=AD) =
to read
the file, UnsatisfiedLink error disappears. However, the read bytes =
cannot
be transformed to String. The code is:=20

         RandomAccessFile rf =3D new CharRandomAccessFile(file, "r");

         byte [] data =3D new byte[4*1024];

         rf.read(data, 0, data.length);

         String s =3D new String(data);

         System.out.println(s);

However, the output to screen is invisible. Note String(byte[]) is to =
decode
bytes with default charset name. Is there a simple approach to transform =
the
bytes to String? Or, do we have to implement a new peer method to read =
file
into a char array?

Re: [Javapathfinder-user] cannot open file in JPF

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

Wm91LAoKeW91IHdpbGwgaGF2ZSB0byBlaXRoZXIgcHJvdmlkZSBhIHBlZXIgaW1wbGVtZW50YXRp
b24gZm9yIHRoZSBuYXRpdmUKbWV0aG9kLCBvciBwcm92aWRlIGEgbW9kZWwgKG9yIHBlZXIpIGlt
cGxlbWVudGF0aW9uIGZvciBzb21ldGhpbmcKYWJvdmUgaXQgaW4gdGhlIGNhbGwgc3RhY2suCgpJ
IHlvdSBhcmUganVzdCByZWFkaW5nIHRoZSBmaWxlIG9uY2UgYXQgaW5pdGlhbGl6YXRpb24sIEkg
d291bGQKY29uc2lkZXIgbW92aW5nIHRoZSBpbXBsZW1lbnRhdGlvbiBvZiB0aGUgcGFyc2UgbWV0
aG9kIGludG8gYSBwZWVyCm1ldGhvZCwgc28gaXQgd2lsbCBydW4gb24gdGhlIEpWTSBhbmQgcmVh
ZCB0aGUgZmlsZSBzeXN0ZW0sIGV0Yy4gIHRoaXMKaGFzIHRoZSBzaWRlIGJlbmVmaXQgb2YgbW92
aW5nIHRoZSBwYXJzZSBjb2RlIG91dCBvZiB0aGUgSlBGIG1lbW9yeSwKd2hpY2ggaGVscHMgcGVy
Zm9ybWFuY2UgKGFzc3VtaW5nIHRoaXMgaXMgbm90IGNvZGUgeW91IGFyZSB0cnlpbmcgdG8KY2hl
Y2spLgoKQW5vdGhlciBwb3NzaWJpbGl0eSB3b3VsZCBiZSB0byBsb29rIGF0IHRoZSBSYW5kb21B
Y2Nlc3NGaWxlIHBlZXIKaW1wbGVtZW50YXRpb24gYW5kIHNlZSBpZiB5b3UgY2FuIHVzZSB0aGF0
IGZ1bmN0aW9uYWxpdHkgdG8gaW1wbGVtZW50CnRoZSB0eXBlIG9mIGZpbGUgYmVoYXZpb3IgeW91
IG5lZWQuCgpKb2huCgpPbiAzLzIwLzA2LCB6dW8gamlob25nIDx6dW9qaEBwa3UuZWR1LmNuPiB3
cm90ZToKPgo+Cj4KPiBJbiBteSBhcHAsIEkgd2FudCB0byBvcGVuIGEgZmlsZSB0byByZWFkIGFu
ZCBwYXJzZSBzb21lIHJ1bGVzLiBIb3dldmVyLCBqcGYKPiB3aWxsIHJlcG9ydCBVbnNhdGlzZmll
ZExpbmsgZXJyb3IuIFRoZSBleGFtcGxlIGlzIGFzIGZvbGxvd3M6Cj4KPgo+Cj4gcHVibGljIHN0
YXRpYyB2b2lkIHBhcnNlKFN0cmluZyBmbikgewo+Cj4gICAgICAgICAgQnVmZmVyZWRSZWFkZXIg
aW4gPSBuZXcgQnVmZmVyZWRSZWFkZXIobmV3IEZpbGVSZWFkZXIoZm4pKTsKPgo+ICAgICAgICAg
IHdoaWxlICh0cnVlKSB7Cj4KPiAgICAgICAgICAgICAgICAgICAgU3RyaW5nIHMgPSBpbi5yZWFk
TGluZSgpOwo+Cj4gICAgICAgICAgICAgICAgICAgIKGtCj4KPiAgICAgICAgICB9Cj4KPiB9Cj4K
Pgo+Cj4gVGhlIG91cHV0IHJlcG9ydHMgYW4gZXJyb3IgbGlrZToKPgo+Cj4KPiAkIGJpbi9qcGYg
bW9kZWwuTWFpbFZlcmlmaWVyIC1pIC4uL2VtYWlsL3J1bGVzCj4KPiBqYXZhLmxhbmcuVW5zYXRp
c2ZpZWRMaW5rRXJyb3I6IGphdmEuaW8uRmlsZUlucHV0U3RyZWFtLmluaXRJRHMgKG5vIHBlZXIp
Cj4KPiAgICAgICAgIGF0Cj4gamF2YS5pby5GaWxlSW5wdXRTdHJlYW0uPGNsaW5pdD4oamF2YVxp
b1xGaWxlSW5wdXRTdHJlYW0uamF2YToyODEpCj4KPiAgICAgICAgIGF0Cj4gamF2YS5pby5GaWxl
UmVhZGVyLjxpbml0PihqYXZhXGlvXEZpbGVSZWFkZXIuamF2YTo0MSkKPgo+ICAgICAgICAgYXQg
bW9kZWwuY2hlY2suUGFyc2VyLnBhcnNlKG1vZGVsXGNoZWNrXFBhcnNlci5qYXZhOjIxKQo+Cj4g
ICAgICAgICBhdCBtb2RlbC5NYWlsVmVyaWZpZXIubWFpbihtb2RlbFxNYWlsVmVyaWZpZXIuamF2
YToxMykKPgo+Cj4KPiBXaGVuIEkgZ2V0IGludG8gdGhlIHNvdXJjZSBjb2RlIG9mIEZpbGVJbnB1
dFN0cmVhbSBJIGdvdCB0aGUgcmVhc29uLiBUaGF0J3MKPiBiZWNhdXNlIGluaXRJRHMgaXMgYSBu
YXRpdmUgZnVuY3Rpb24gb2YgRmlsZUlucHV0U3RyZWFtLiBBcyB0aGUgY29kZSBpcwo+IGV4ZWN1
dGVkIHVuZGVyIGpwZiwganBmIHdpbGwgdHJ5IHRvIHNlYXJjaCB0aGUgY29ycmVzcG9uZGluZwo+
IEpQRl9qYXZhX2lvX0ZpbGVJbnB1dFN0cmVhbS5pbml0SURzKCkgYW5kIHN1cmVseSBmYWlscy4g
U28sCj4gd2hhdCBjYW4gSSBkbyB0byBnZXQgYXJvdW5kIHRoaXM/IFRoYW5rIGZvciBoZWxwIQo+
Cj4KPgo+IEouIEguIFp1bwo=

[Javapathfinder-user] cannot open file in JPF

[zuo j. <zu...@pk...>]

In my app, I want to open a file to read and parse some rules. However, =
jpf
will report UnsatisfiedLink error. The example is as follows:

=20

public static void parse(String fn) {

         BufferedReader in =3D new BufferedReader(new FileReader(fn));

         while (true) {

                   String s =3D in.readLine();

                   =A1=AD

         }

}

=20

The ouput reports an error like:

=20

$ bin/jpf model.MailVerifier -i ../email/rules

java.lang.UnsatisfiedLinkError: java.io.FileInputStream.initIDs (no =
peer)

        at
java.io.FileInputStream.<clinit>(java\io\FileInputStream.java:281)

        at java.io.FileReader.<init>(java\io\FileReader.java:41)

        at model.check.Parser.parse(model\check\Parser.java:21)

        at model.MailVerifier.main(model\MailVerifier.java:13)

=20

When I get into the source code of FileInputStream I got the reason. =
That=A1=AFs
because initIDs is a native function of FileInputStream. As the code is
executed under jpf, jpf will try to search the corresponding
JPF_java_io_FileInputStream.initIDs() and surely fails. So, what can I =
do to
get around this? Thank for help!

=20

J. H. Zuo

[Javapathfinder-user] contracts in javapathfinder

[harry h. <har...@ho...>]

Hi,

I have a question how to write the precondtion, postcondition and class 
invariant in the java pathfinder. Can we write the code semantics( 
precondtion, postcondition and class invariant )  like JML in java 
pathfinder ?

harry

Re: [Javapathfinder-user] Testing the deadlock

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

Hi Harry,

I think that is the BCEL compatability problem - the BCEL version on
the JPF sourceforge site should fix this.

John

On 3/13/06, harry huang <har...@ho...> wrote:
> 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 folde=
r.
> The  "java deadlock.Deadlock" passed and give me the output like in below=
 :
>
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
> B.foo() was called
> B cycle start
> A cycle end
> A.foo() was called
> A cycle start
> B cycle end
> B.foo() was called
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
> However, when I executed "jpf deadlock.Deadlock", there are exceptions
> thrown :
>
> =3D=3D=3D=3D=3D=3D=3D=3D
> 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:22=
1)
>         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:208=
1)
>         at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
>         at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:28=
5)
>         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.StringIndexOutOfBoundsExcepti=
on:
> 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:208=
1)
>         at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
>         at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:28=
5)
>         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:208=
1)
>         at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1565)
>         at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:28=
5)
>         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.StringIndexOutOfBoundsExceptio=
n:
> 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)
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
>
> Can someone give me some advices and how to fix it ?
>
> Thanks.
> Harry
>
>
>
>
> -------------------------------------------------------
> This SF.Net email is sponsored by xPML, a groundbreaking scripting langua=
ge
> that extends applications into web and mobile media. Attend the live webc=
ast
> and join the prime developer group breaking into this new coding territor=
y!
> http://sel.as-us.falkag.net/sel?cmd=3Dlnk&kid=3D110944&bid=3D241720&dat=
=3D121642
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

[Javapathfinder-user] How to detect deadlock

[harry h. <har...@ho...>]

Hi ,

I am a new to this product. I just have a question. Suppose I have a java 
program called A like below:

====
Public class A
{
     public A()
    { ... }

    public void B()
    {
        C();
     }

    public void C()
   {  ... }
}
=======
There might be a deadlock occurs at the method C(). How can I use java 
Pathfinder to detect the deadlock. Can some one give me some draft java 
pathfinder code to detect the deadlock ? I do not have much ideas regarding 
the java pathfinder program .

Harry

[Javapathfinder-user] Testing the deadlock

[harry h. <har...@ho...>]

Sorry , just ingore below one.

Harry
===========

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

[Javapathfinder-user] Testing the deadlock

[harry h. <har...@ho...>]

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

[Javapathfinder-user] JPF installation

[Ali T. <ata...@cs...>]

Hi,
I am trying to install and use JPF. I have completed all steps. When I try to
run the program however I get the following error:

"Error occured during initialization of VM"
"Could not reserve enough space for object heap"

I would appreciate if you could help me out.
thanks
Ali

-- 
Ali Taleghani
PhD Candidate
School of Computer Science
University of Waterloo
DC 3320

----------------------------------------
This mail sent through www.mywaterloo.ca

RE: [Javapathfinder-user] Testing the deadlock

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

Hi Harry,

JPF is not working correctly with Java 1.5 yet. We thought we had it
nailed but it turned out newer versions of the library code breaks JPF.
The good news is that we are very nearly finished with a version that is
fully 1.5 compatible. For the time being use 1.4 and all will be well.

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
> harry huang
> Sent: Monday, March 13, 2006 7:17 AM
> To: jav...@li...
> Subject: [Javapathfinder-user] Testing the deadlock
> 
> 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
> 
> 
> 
> 
> -------------------------------------------------------
> 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