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: Peter C. M. <pcm...@em...> - 2007-10-09 18:44:25
|
what kind of map is this (HashMap, type parameters)? One thing could be that the hashcode() or equals() implementation differs between our lib model and the host VM. -- Peter |
|
From: John P. <jp...@go...> - 2007-10-09 16:58:15
|
Hi Jantien, That could be a bug in JPF. Are you using the same compiler in both cases? John |
|
From: John P. <jp...@go...> - 2007-10-09 16:40:51
|
Hi Jantien,
That could be a bug in JPF. Are you using the same compiler in both cases?
John
On 10/9/07, Jantien Sessink <jan...@gx...> wrote:
>
> Hi,
>
>
>
> Last week I posted the mail below. Is there anyone who knows the answer
> already? Am I doing something wrong, or is there a bug in JPF?
>
>
>
> Kind regards,
>
> Jantien Sessink
>
>
> ------------------------------
>
> *From:* jav...@li... [mailto:
> jav...@li...] *On Behalf Of *Jantien
> Sessink
> *Sent:* Friday, October 05, 2007 3:51 PM
> *To:* jav...@li...
> *Subject:* [Javapathfinder-user] Bug in JPF or in my code?????
>
>
>
> Hi,
>
>
>
> I don't know if I have encountered a bug in JPF or that I'm doing
> something wrong. I have a program that uses the Map class from java.util.
> At some point I check if a key exists in the Map. This raises an exception
> when I run it in JPF while Eclipse runs the program without any exceptions.
>
> I wrote the keys in the map and the key names derived from an array to the
> screen to check if the keys from the array (ntNames) exist in the map
> (ntdCache). As can be seen in the output of JPF below, the name in ntNames
> exists in ntdCache, while ntdCache.containsKey(ntNames[i]) returns false
> and reassess an exception. This is strange. But when I run the program in
> Eclipse, there are no exceptions. The part of code that creates the
> exception:
>
>
>
> for (int i = 0; i < ntNames.length; i++) {
>
> if (!ntdCache.containsKey(ntNames[i])) {
>
> throw new NoSuchNodeTypeException(ntNames[i].toString());
>
> }
>
> }
>
>
>
> The outcome of Eclipse and JPF are below.
>
> I hope someone can help me, because I don't know if the problem is in my
> code or in JPF. If any of the above is not clear, I can give more
> explanation.
>
>
>
> Kind regards,
>
> Jantien Sessink
>
>
>
> ------------------------------------- JPF
> -----------------------------------------------------------------
>
> JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
>
>
>
>
>
> ====================================================== system under test
>
> application: nl.gx.firsthop.FirstHop.class
>
>
>
> ====================================================== search started:
> 10/5/07 1:06 PM
>
> 1172 [main] INFO org.apache.jackrabbit.core.RepositoryImpl - Starting
> repository...
>
> Printing names from ntNames:
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> Printing names from ntdCache:
>
> {internal}versionStorage
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}versionedChild<http://www.jcp.org/jcr/nt/1.0%7DversionedChild>
>
> {http://www.jcp.org/jcr/nt/1.0}versionLabels<http://www.jcp.org/jcr/nt/1.0%7DversionLabels>
>
> {http://www.jcp.org/jcr/nt/1.0}childNodeDefinition<http://www.jcp.org/jcr/nt/1.0%7DchildNodeDefinition>
>
> {http://www.jcp.org/jcr/mix/1.0}versionable<http://www.jcp.org/jcr/mix/1.0%7Dversionable>
>
> {http://www.jcp.org/jcr/nt/1.0}resource<http://www.jcp.org/jcr/nt/1.0%7Dresource>
>
> {http://www.jcp.org/jcr/nt/1.0}file <http://www.jcp.org/jcr/nt/1.0%7Dfile>
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> {http://www.jcp.org/jcr/nt/1.0}versionHistory<http://www.jcp.org/jcr/nt/1.0%7DversionHistory>
>
> {http://www.jcp.org/jcr/nt/1.0}version<http://www.jcp.org/jcr/nt/1.0%7Dversion>
>
> {http://www.jcp.org/jcr/nt/1.0}linkedFile<http://www.jcp.org/jcr/nt/1.0%7DlinkedFile>
>
> {internal}root
>
> {internal}nodeTypes
>
> {http://www.jcp.org/jcr/nt/1.0}propertyDefinition<http://www.jcp.org/jcr/nt/1.0%7DpropertyDefinition>
>
> {http://www.jcp.org/jcr/nt/1.0}frozenNode<http://www.jcp.org/jcr/nt/1.0%7DfrozenNode>
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> {http://www.jcp.org/jcr/nt/1.0}nodeType<http://www.jcp.org/jcr/nt/1.0%7DnodeType>
>
> {http://www.jcp.org/jcr/nt/1.0}query<http://www.jcp.org/jcr/nt/1.0%7Dquery>
>
> {internal}system
>
> {http://www.jcp.org/jcr/mix/1.0}lockable<http://www.jcp.org/jcr/mix/1.0%7Dlockable>
>
> {http://www.jcp.org/jcr/nt/1.0}folder<http://www.jcp.org/jcr/nt/1.0%7Dfolder>
>
> Printing names from ntNames:
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> Printing names from ntdCache:
>
> {internal}versionStorage
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}versionedChild<http://www.jcp.org/jcr/nt/1.0%7DversionedChild>
>
> {http://www.jcp.org/jcr/nt/1.0}versionLabels<http://www.jcp.org/jcr/nt/1.0%7DversionLabels>
>
> {http://www.jcp.org/jcr/nt/1.0}childNodeDefinition<http://www.jcp.org/jcr/nt/1.0%7DchildNodeDefinition>
>
> {http://www.jcp.org/jcr/mix/1.0}versionable<http://www.jcp.org/jcr/mix/1.0%7Dversionable>
>
> {http://www.jcp.org/jcr/nt/1.0}resource<http://www.jcp.org/jcr/nt/1.0%7Dresource>
>
> {http://www.jcp.org/jcr/nt/1.0}file <http://www.jcp.org/jcr/nt/1.0%7Dfile>
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> {http://www.jcp.org/jcr/nt/1.0}versionHistory<http://www.jcp.org/jcr/nt/1.0%7DversionHistory>
>
> {http://www.jcp.org/jcr/nt/1.0}version<http://www.jcp.org/jcr/nt/1.0%7Dversion>
>
> {http://www.jcp.org/jcr/nt/1.0}linkedFile<http://www.jcp.org/jcr/nt/1.0%7DlinkedFile>
>
> {internal}root
>
> {internal}nodeTypes
>
> {http://www.jcp.org/jcr/nt/1.0}propertyDefinition<http://www.jcp.org/jcr/nt/1.0%7DpropertyDefinition>
>
> {http://www.jcp.org/jcr/nt/1.0}frozenNode<http://www.jcp.org/jcr/nt/1.0%7DfrozenNode>
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> {http://www.jcp.org/jcr/nt/1.0}nodeType<http://www.jcp.org/jcr/nt/1.0%7DnodeType>
>
> {http://www.jcp.org/jcr/nt/1.0}query<http://www.jcp.org/jcr/nt/1.0%7Dquery>
>
> {internal}system
>
> {http://www.jcp.org/jcr/mix/1.0}lockable<http://www.jcp.org/jcr/mix/1.0%7Dlockable>
>
> {http://www.jcp.org/jcr/nt/1.0}folder<http://www.jcp.org/jcr/nt/1.0%7Dfolder>
>
> org.apache.jackrabbit.core.nodetype.InvalidNodeTypeDefException:
> [{internal}versionStorage] failed to validate supertype
>
> s
>
> at
> org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.validateNodeTypeDef(
> NodeTypeRegistry.java:1485)
>
> at
> org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.internalRegister(
> NodeTypeRegistry.java:1311)
>
> at org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(
> NodeTypeRegistry.java:746)
>
> at org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(
> NodeTypeRegistry.java:120)
>
> at
> org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(
> RepositoryImpl.java:515)
>
> at org.apache.jackrabbit.core.RepositoryImpl.<init>(
> RepositoryImpl.java:262)
>
> at org.apache.jackrabbit.core.RepositoryImpl.create(
> RepositoryImpl.java:528)
>
> at org.apache.jackrabbit.core.TransientRepository$2.getRepository(
> TransientRepository.java:249)
>
> at org.apache.jackrabbit.core.TransientRepository.startRepository(
> TransientRepository.java:270)
>
> at org.apache.jackrabbit.core.TransientRepository.login(
> TransientRepository.java:338)
>
> at org.apache.jackrabbit.core.TransientRepository.login(
> TransientRepository.java:368)
>
> at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
>
> Caused by: javax.jcr.nodetype.NoSuchNodeTypeException: {
> http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> at
> org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.getEffectiveNodeType(
> NodeTypeRegistry.java:1079)
>
> at org.apache.jackrabbit.core.nodetype.EffectiveNodeType.create(
> EffectiveNodeType.java:202)
>
> at
> org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.getEffectiveNodeType(
> NodeTypeRegistry.java:1110)
>
> at
> org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.validateNodeTypeDef(
> NodeTypeRegistry.java:1469)
>
> at
> org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.internalRegister(
> NodeTypeRegistry.java:1311)
>
> at org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(
> NodeTypeRegistry.java:746)
>
> at org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(
> NodeTypeRegistry.java:120)
>
> at
> org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(
> RepositoryImpl.java:515)
>
> at org.apache.jackrabbit.core.RepositoryImpl.<init>(
> RepositoryImpl.java:262)
>
> at org.apache.jackrabbit.core.RepositoryImpl.create(
> RepositoryImpl.java:528)
>
> at org.apache.jackrabbit.core.TransientRepository$2.getRepository(
> TransientRepository.java:249)
>
> at org.apache.jackrabbit.core.TransientRepository.startRepository(
> TransientRepository.java:270)
>
> at org.apache.jackrabbit.core.TransientRepository.login(
> TransientRepository.java:338)
>
> at org.apache.jackrabbit.core.TransientRepository.login(
> TransientRepository.java:368)
>
> at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
>
>
>
> ====================================================== error #1
>
> gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
>
> javax.jcr.RepositoryException: internal error: invalid built-in node type
> definition stored in org/apache/jackrabbit/cor
>
> e/nodetype/builtin_nodetypes.xml
>
> at org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(
> NodeTypeRegistry.java:753)
>
> at org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(
> NodeTypeRegistry.java:120)
>
> at
> org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(
> RepositoryImpl.java:515)
>
> at org.apache.jackrabbit.core.RepositoryImpl.<init>(
> RepositoryImpl.java:262)
>
> at org.apache.jackrabbit.core.RepositoryImpl.create(
> RepositoryImpl.java:528)
>
> at org.apache.jackrabbit.core.TransientRepository$2.getRepository(
> TransientRepository.java:249)
>
> at org.apache.jackrabbit.core.TransientRepository.startRepository(
> TransientRepository.java:270)
>
> at org.apache.jackrabbit.core.TransientRepository.login(
> TransientRepository.java:338)
>
> at org.apache.jackrabbit.core.TransientRepository.login(
> TransientRepository.java:368)
>
> at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
>
>
>
>
>
> ====================================================== trace #1
>
> ------------------------------------------------------ transition #0
> thread: 0
>
> gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
>
>
>
> ====================================================== snapshot #1
>
> no live threads
>
>
>
> ====================================================== results
>
> error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "
> javax.jcr.RepositoryException: internal error: inv..."
>
>
>
> ====================================================== search finished:
> 10/5/07 1:07 PM
>
>
>
> ---------------------------------------------------- End JPF
> ---------------------------------------------------
>
>
>
> ---------------------------------------------------- Eclipse
> ---------------------------------------------------
>
> Printing names from ntNames:
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> Printing names from ntdCache:
>
> {internal}versionStorage
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}versionedChild<http://www.jcp.org/jcr/nt/1.0%7DversionedChild>
>
> {http://www.jcp.org/jcr/nt/1.0}versionLabels<http://www.jcp.org/jcr/nt/1.0%7DversionLabels>
>
> {http://www.jcp.org/jcr/nt/1.0}childNodeDefinition<http://www.jcp.org/jcr/nt/1.0%7DchildNodeDefinition>
>
> {http://www.jcp.org/jcr/mix/1.0}versionable<http://www.jcp.org/jcr/mix/1.0%7Dversionable>
>
> {http://www.jcp.org/jcr/nt/1.0}resource<http://www.jcp.org/jcr/nt/1.0%7Dresource>
>
> {http://www.jcp.org/jcr/nt/1.0}file <http://www.jcp.org/jcr/nt/1.0%7Dfile>
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> {http://www.jcp.org/jcr/nt/1.0}versionHistory<http://www.jcp.org/jcr/nt/1.0%7DversionHistory>
>
> {http://www.jcp.org/jcr/nt/1.0}version<http://www.jcp.org/jcr/nt/1.0%7Dversion>
>
> {http://www.jcp.org/jcr/nt/1.0}linkedFile<http://www.jcp.org/jcr/nt/1.0%7DlinkedFile>
>
> {internal}root
>
> {internal}nodeTypes
>
> {http://www.jcp.org/jcr/nt/1.0}propertyDefinition<http://www.jcp.org/jcr/nt/1.0%7DpropertyDefinition>
>
> {http://www.jcp.org/jcr/nt/1.0}frozenNode<http://www.jcp.org/jcr/nt/1.0%7DfrozenNode>
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> {http://www.jcp.org/jcr/nt/1.0}nodeType<http://www.jcp.org/jcr/nt/1.0%7DnodeType>
>
> {http://www.jcp.org/jcr/nt/1.0}query<http://www.jcp.org/jcr/nt/1.0%7Dquery>
>
> {internal}system
>
> {http://www.jcp.org/jcr/mix/1.0}lockable<http://www.jcp.org/jcr/mix/1.0%7Dlockable>
>
> {http://www.jcp.org/jcr/nt/1.0}folder<http://www.jcp.org/jcr/nt/1.0%7Dfolder>
>
> Printing names from ntNames:
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> Printing names from ntdCache:
>
> {internal}versionStorage
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}versionedChild<http://www.jcp.org/jcr/nt/1.0%7DversionedChild>
>
> {http://www.jcp.org/jcr/nt/1.0}versionLabels<http://www.jcp.org/jcr/nt/1.0%7DversionLabels>
>
> {http://www.jcp.org/jcr/nt/1.0}childNodeDefinition<http://www.jcp.org/jcr/nt/1.0%7DchildNodeDefinition>
>
> {http://www.jcp.org/jcr/mix/1.0}versionable<http://www.jcp.org/jcr/mix/1.0%7Dversionable>
>
> {http://www.jcp.org/jcr/nt/1.0}resource<http://www.jcp.org/jcr/nt/1.0%7Dresource>
>
> {http://www.jcp.org/jcr/nt/1.0}file <http://www.jcp.org/jcr/nt/1.0%7Dfile>
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> {http://www.jcp.org/jcr/nt/1.0}versionHistory<http://www.jcp.org/jcr/nt/1.0%7DversionHistory>
>
> {http://www.jcp.org/jcr/nt/1.0}version<http://www.jcp.org/jcr/nt/1.0%7Dversion>
>
> {http://www.jcp.org/jcr/nt/1.0}linkedFile<http://www.jcp.org/jcr/nt/1.0%7DlinkedFile>
>
> {internal}root
>
> {internal}nodeTypes
>
> {http://www.jcp.org/jcr/nt/1.0}propertyDefinition<http://www.jcp.org/jcr/nt/1.0%7DpropertyDefinition>
>
> {http://www.jcp.org/jcr/nt/1.0}frozenNode<http://www.jcp.org/jcr/nt/1.0%7DfrozenNode>
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> {http://www.jcp.org/jcr/nt/1.0}nodeType<http://www.jcp.org/jcr/nt/1.0%7DnodeType>
>
> {http://www.jcp.org/jcr/nt/1.0}query<http://www.jcp.org/jcr/nt/1.0%7Dquery>
>
> {internal}system
>
> {http://www.jcp.org/jcr/mix/1.0}lockable<http://www.jcp.org/jcr/mix/1.0%7Dlockable>
>
> {http://www.jcp.org/jcr/nt/1.0}folder<http://www.jcp.org/jcr/nt/1.0%7Dfolder>
>
> Printing names from ntNames:
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> Printing names from ntdCache:
>
> {internal}versionStorage
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}versionedChild<http://www.jcp.org/jcr/nt/1.0%7DversionedChild>
>
> {http://www.jcp.org/jcr/nt/1.0}versionLabels<http://www.jcp.org/jcr/nt/1.0%7DversionLabels>
>
> {http://www.jcp.org/jcr/nt/1.0}childNodeDefinition<http://www.jcp.org/jcr/nt/1.0%7DchildNodeDefinition>
>
> {http://www.jcp.org/jcr/mix/1.0}versionable<http://www.jcp.org/jcr/mix/1.0%7Dversionable>
>
> {http://www.jcp.org/jcr/nt/1.0}resource<http://www.jcp.org/jcr/nt/1.0%7Dresource>
>
> {http://www.jcp.org/jcr/nt/1.0}file <http://www.jcp.org/jcr/nt/1.0%7Dfile>
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> {http://www.jcp.org/jcr/nt/1.0}versionHistory<http://www.jcp.org/jcr/nt/1.0%7DversionHistory>
>
> {http://www.jcp.org/jcr/nt/1.0}version<http://www.jcp.org/jcr/nt/1.0%7Dversion>
>
> {http://www.jcp.org/jcr/nt/1.0}linkedFile<http://www.jcp.org/jcr/nt/1.0%7DlinkedFile>
>
> {internal}root
>
> {internal}nodeTypes
>
> {http://www.jcp.org/jcr/nt/1.0}propertyDefinition<http://www.jcp.org/jcr/nt/1.0%7DpropertyDefinition>
>
> {http://www.jcp.org/jcr/nt/1.0}frozenNode<http://www.jcp.org/jcr/nt/1.0%7DfrozenNode>
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> {http://www.jcp.org/jcr/nt/1.0}nodeType<http://www.jcp.org/jcr/nt/1.0%7DnodeType>
>
> {http://www.jcp.org/jcr/nt/1.0}query<http://www.jcp.org/jcr/nt/1.0%7Dquery>
>
> {internal}system
>
> {http://www.jcp.org/jcr/mix/1.0}lockable<http://www.jcp.org/jcr/mix/1.0%7Dlockable>
>
> {http://www.jcp.org/jcr/nt/1.0}folder<http://www.jcp.org/jcr/nt/1.0%7Dfolder>
>
> Printing names from ntNames:
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> Printing names from ntdCache:
>
> {internal}versionStorage
>
> {http://www.jcp.org/jcr/mix/1.0}referenceable<http://www.jcp.org/jcr/mix/1.0%7Dreferenceable>
>
> {http://www.jcp.org/jcr/nt/1.0}versionedChild<http://www.jcp.org/jcr/nt/1.0%7DversionedChild>
>
> {http://www.jcp.org/jcr/nt/1.0}versionLabels<http://www.jcp.org/jcr/nt/1.0%7DversionLabels>
>
> {http://www.jcp.org/jcr/nt/1.0}childNodeDefinition<http://www.jcp.org/jcr/nt/1.0%7DchildNodeDefinition>
>
> {http://www.jcp.org/jcr/mix/1.0}versionable<http://www.jcp.org/jcr/mix/1.0%7Dversionable>
>
> {http://www.jcp.org/jcr/nt/1.0}resource<http://www.jcp.org/jcr/nt/1.0%7Dresource>
>
> {http://www.jcp.org/jcr/nt/1.0}file <http://www.jcp.org/jcr/nt/1.0%7Dfile>
>
> {http://www.jcp.org/jcr/nt/1.0}hierarchyNode<http://www.jcp.org/jcr/nt/1.0%7DhierarchyNode>
>
> {http://www.jcp.org/jcr/nt/1.0}base <http://www.jcp.org/jcr/nt/1.0%7Dbase>
>
> {http://www.jcp.org/jcr/nt/1.0}versionHistory<http://www.jcp.org/jcr/nt/1.0%7DversionHistory>
>
> {http://www.jcp.org/jcr/nt/1.0}version<http://www.jcp.org/jcr/nt/1.0%7Dversion>
>
> {http://www.jcp.org/jcr/nt/1.0}linkedFile<http://www.jcp.org/jcr/nt/1.0%7DlinkedFile>
>
> {internal}root
>
> {internal}nodeTypes
>
> {http://www.jcp.org/jcr/nt/1.0}propertyDefinition<http://www.jcp.org/jcr/nt/1.0%7DpropertyDefinition>
>
> {http://www.jcp.org/jcr/nt/1.0}frozenNode<http://www.jcp.org/jcr/nt/1.0%7DfrozenNode>
>
> {http://www.jcp.org/jcr/nt/1.0}unstructured<http://www.jcp.org/jcr/nt/1.0%7Dunstructured>
>
> {http://www.jcp.org/jcr/nt/1.0}nodeType<http://www.jcp.org/jcr/nt/1.0%7DnodeType>
>
> {http://www.jcp.org/jcr/nt/1.0}query<http://www.jcp.org/jcr/nt/1.0%7Dquery>
>
> {internal}system
>
> {http://www.jcp.org/jcr/mix/1.0}lockable<http://www.jcp.org/jcr/mix/1.0%7Dlockable>
>
> {http://www.jcp.org/jcr/nt/1.0}folder<http://www.jcp.org/jcr/nt/1.0%7Dfolder>
>
>
>
> ----------------------------------------------------- End Eclipse
> ---------------------------------------------
>
>
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Splunk Inc.
> Still grepping through log files to find problems? Stop.
> Now Search log events and configuration files using AJAX and a browser.
> Download your FREE copy of Splunk now >> http://get.splunk.com/
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>
>
|
|
From: Jantien S. <jan...@gx...> - 2007-10-09 13:13:49
|
Hi,
=20
Last week I posted the mail below. Is there anyone who knows the answer
already? Am I doing something wrong, or is there a bug in JPF?
=20
Kind regards,
Jantien Sessink
=20
________________________________
From: jav...@li...
[mailto:jav...@li...] On Behalf Of
Jantien Sessink
Sent: Friday, October 05, 2007 3:51 PM
To: jav...@li...
Subject: [Javapathfinder-user] Bug in JPF or in my code?????
=20
Hi,
=20
I don't know if I have encountered a bug in JPF or that I'm doing
something wrong. I have a program that uses the Map class from
java.util. At some point I check if a key exists in the Map. This raises
an exception when I run it in JPF while Eclipse runs the program without
any exceptions.=20
I wrote the keys in the map and the key names derived from an array to
the screen to check if the keys from the array (ntNames) exist in the
map (ntdCache). As can be seen in the output of JPF below, the name in
ntNames exists in ntdCache, while ntdCache.containsKey(ntNames[i])
returns false and reassess an exception. This is strange. But when I run
the program in Eclipse, there are no exceptions. The part of code that
creates the exception:
=20
for (int i =3D 0; i < ntNames.length; i++) {
if (!ntdCache.containsKey(ntNames[i])) {
throw new NoSuchNodeTypeException(ntNames[i].toString());
}
}
=20
The outcome of Eclipse and JPF are below.
I hope someone can help me, because I don't know if the problem is in my
code or in JPF. If any of the above is not clear, I can give more
explanation.
=20
Kind regards,
Jantien Sessink
=20
------------------------------------- JPF
-----------------------------------------------------------------
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
=20
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D system under test
application: nl.gx.firsthop.FirstHop.class
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search started:
10/5/07 1:06 PM
1172 [main] INFO org.apache.jackrabbit.core.RepositoryImpl - Starting
repository...
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
org.apache.jackrabbit.core.nodetype.InvalidNodeTypeDefException:
[{internal}versionStorage] failed to validate supertype
s
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.validateNodeTypeDef
(NodeTypeRegistry.java:1485)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.internalRegister(No
deTypeRegistry.java:1311)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(NodeTypeRegi
stry.java:746)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(NodeTypeRegi
stry.java:120)
at
org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(Reposit
oryImpl.java:515)
at
org.apache.jackrabbit.core.RepositoryImpl.<init>(RepositoryImpl.java:262
)
at
org.apache.jackrabbit.core.RepositoryImpl.create(RepositoryImpl.java:528
)
at
org.apache.jackrabbit.core.TransientRepository$2.getRepository(Transient
Repository.java:249)
at
org.apache.jackrabbit.core.TransientRepository.startRepository(Transient
Repository.java:270)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:338)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:368)
at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
Caused by: javax.jcr.nodetype.NoSuchNodeTypeException:
{http://www.jcp.org/jcr/nt/1.0}base
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.getEffectiveNodeTyp
e(NodeTypeRegistry.java:1079)
at
org.apache.jackrabbit.core.nodetype.EffectiveNodeType.create(EffectiveNo
deType.java:202)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.getEffectiveNodeTyp
e(NodeTypeRegistry.java:1110)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.validateNodeTypeDef
(NodeTypeRegistry.java:1469)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.internalRegister(No
deTypeRegistry.java:1311)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(NodeTypeRegi
stry.java:746)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(NodeTypeRegi
stry.java:120)
at
org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(Reposit
oryImpl.java:515)
at
org.apache.jackrabbit.core.RepositoryImpl.<init>(RepositoryImpl.java:262
)
at
org.apache.jackrabbit.core.RepositoryImpl.create(RepositoryImpl.java:528
)
at
org.apache.jackrabbit.core.TransientRepository$2.getRepository(Transient
Repository.java:249)
at
org.apache.jackrabbit.core.TransientRepository.startRepository(Transient
Repository.java:270)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:338)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:368)
at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
javax.jcr.RepositoryException: internal error: invalid built-in node
type definition stored in org/apache/jackrabbit/cor
e/nodetype/builtin_nodetypes.xml
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(NodeTypeRegi
stry.java:753)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(NodeTypeRegi
stry.java:120)
at
org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(Reposit
oryImpl.java:515)
at
org.apache.jackrabbit.core.RepositoryImpl.<init>(RepositoryImpl.java:262
)
at
org.apache.jackrabbit.core.RepositoryImpl.create(RepositoryImpl.java:528
)
at
org.apache.jackrabbit.core.TransientRepository$2.getRepository(Transient
Repository.java:249)
at
org.apache.jackrabbit.core.TransientRepository.startRepository(Transient
Repository.java:270)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:338)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:368)
at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
=20
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D trace #1
------------------------------------------------------ transition #0
thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D snapshot #1
no live threads
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
"javax.jcr.RepositoryException: internal error: inv..."
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search finished:
10/5/07 1:07 PM
=20
---------------------------------------------------- End JPF
---------------------------------------------------
=20
---------------------------------------------------- Eclipse
---------------------------------------------------
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}unstructured
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
=20
----------------------------------------------------- End Eclipse
---------------------------------------------
=20
|
|
From: Jantien S. <jan...@gx...> - 2007-10-05 13:51:26
|
Hi,
=20
I don't know if I have encountered a bug in JPF or that I'm doing
something wrong. I have a program that uses the Map class from
java.util. At some point I check if a key exists in the Map. This raises
an exception when I run it in JPF while Eclipse runs the program without
any exceptions.=20
I wrote the keys in the map and the key names derived from an array to
the screen to check if the keys from the array (ntNames) exist in the
map (ntdCache). As can be seen in the output of JPF below, the name in
ntNames exists in ntdCache, while ntdCache.containsKey(ntNames[i])
returns false and reassess an exception. This is strange. But when I run
the program in Eclipse, there are no exceptions. The part of code that
creates the exception:
=20
for (int i =3D 0; i < ntNames.length; i++) {
if (!ntdCache.containsKey(ntNames[i])) {
throw new NoSuchNodeTypeException(ntNames[i].toString());
}
}
=20
The outcome of Eclipse and JPF are below.
I hope someone can help me, because I don't know if the problem is in my
code or in JPF. If any of the above is not clear, I can give more
explanation.
=20
Kind regards,
Jantien Sessink
=20
------------------------------------- JPF
-----------------------------------------------------------------
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
=20
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D system under test
application: nl.gx.firsthop.FirstHop.class
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search started:
10/5/07 1:06 PM
1172 [main] INFO org.apache.jackrabbit.core.RepositoryImpl - Starting
repository...
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
org.apache.jackrabbit.core.nodetype.InvalidNodeTypeDefException:
[{internal}versionStorage] failed to validate supertype
s
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.validateNodeTypeDef
(NodeTypeRegistry.java:1485)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.internalRegister(No
deTypeRegistry.java:1311)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(NodeTypeRegi
stry.java:746)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(NodeTypeRegi
stry.java:120)
at
org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(Reposit
oryImpl.java:515)
at
org.apache.jackrabbit.core.RepositoryImpl.<init>(RepositoryImpl.java:262
)
at
org.apache.jackrabbit.core.RepositoryImpl.create(RepositoryImpl.java:528
)
at
org.apache.jackrabbit.core.TransientRepository$2.getRepository(Transient
Repository.java:249)
at
org.apache.jackrabbit.core.TransientRepository.startRepository(Transient
Repository.java:270)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:338)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:368)
at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
Caused by: javax.jcr.nodetype.NoSuchNodeTypeException:
{http://www.jcp.org/jcr/nt/1.0}base
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.getEffectiveNodeTyp
e(NodeTypeRegistry.java:1079)
at
org.apache.jackrabbit.core.nodetype.EffectiveNodeType.create(EffectiveNo
deType.java:202)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.getEffectiveNodeTyp
e(NodeTypeRegistry.java:1110)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.validateNodeTypeDef
(NodeTypeRegistry.java:1469)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.internalRegister(No
deTypeRegistry.java:1311)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(NodeTypeRegi
stry.java:746)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(NodeTypeRegi
stry.java:120)
at
org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(Reposit
oryImpl.java:515)
at
org.apache.jackrabbit.core.RepositoryImpl.<init>(RepositoryImpl.java:262
)
at
org.apache.jackrabbit.core.RepositoryImpl.create(RepositoryImpl.java:528
)
at
org.apache.jackrabbit.core.TransientRepository$2.getRepository(Transient
Repository.java:249)
at
org.apache.jackrabbit.core.TransientRepository.startRepository(Transient
Repository.java:270)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:338)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:368)
at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
javax.jcr.RepositoryException: internal error: invalid built-in node
type definition stored in org/apache/jackrabbit/cor
e/nodetype/builtin_nodetypes.xml
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.<init>(NodeTypeRegi
stry.java:753)
at
org.apache.jackrabbit.core.nodetype.NodeTypeRegistry.create(NodeTypeRegi
stry.java:120)
at
org.apache.jackrabbit.core.RepositoryImpl.createNodeTypeRegistry(Reposit
oryImpl.java:515)
at
org.apache.jackrabbit.core.RepositoryImpl.<init>(RepositoryImpl.java:262
)
at
org.apache.jackrabbit.core.RepositoryImpl.create(RepositoryImpl.java:528
)
at
org.apache.jackrabbit.core.TransientRepository$2.getRepository(Transient
Repository.java:249)
at
org.apache.jackrabbit.core.TransientRepository.startRepository(Transient
Repository.java:270)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:338)
at
org.apache.jackrabbit.core.TransientRepository.login(TransientRepository
.java:368)
at nl.gx.firsthop.FirstHop.main(FirstHop.java:31)
=20
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D trace #1
------------------------------------------------------ transition #0
thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D snapshot #1
no live threads
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
"javax.jcr.RepositoryException: internal error: inv..."
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search finished:
10/5/07 1:07 PM
=20
---------------------------------------------------- End JPF
---------------------------------------------------
=20
---------------------------------------------------- Eclipse
---------------------------------------------------
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}base
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
Printing names from ntNames:
{http://www.jcp.org/jcr/nt/1.0}unstructured
Printing names from ntdCache:
{internal}versionStorage
{http://www.jcp.org/jcr/mix/1.0}referenceable
{http://www.jcp.org/jcr/nt/1.0}versionedChild
{http://www.jcp.org/jcr/nt/1.0}versionLabels
{http://www.jcp.org/jcr/nt/1.0}childNodeDefinition
{http://www.jcp.org/jcr/mix/1.0}versionable
{http://www.jcp.org/jcr/nt/1.0}resource
{http://www.jcp.org/jcr/nt/1.0}file
{http://www.jcp.org/jcr/nt/1.0}hierarchyNode
{http://www.jcp.org/jcr/nt/1.0}base
{http://www.jcp.org/jcr/nt/1.0}versionHistory
{http://www.jcp.org/jcr/nt/1.0}version
{http://www.jcp.org/jcr/nt/1.0}linkedFile
{internal}root
{internal}nodeTypes
{http://www.jcp.org/jcr/nt/1.0}propertyDefinition
{http://www.jcp.org/jcr/nt/1.0}frozenNode
{http://www.jcp.org/jcr/nt/1.0}unstructured
{http://www.jcp.org/jcr/nt/1.0}nodeType
{http://www.jcp.org/jcr/nt/1.0}query
{internal}system
{http://www.jcp.org/jcr/mix/1.0}lockable
{http://www.jcp.org/jcr/nt/1.0}folder
=20
----------------------------------------------------- End Eclipse
---------------------------------------------
=20
|
|
From: Jantien S. <jan...@gx...> - 2007-09-26 07:21:49
|
Hi, =20 I have a problem with giving objects back from the Native class to the Model class. The Model class calls a function in the Native class that creates a session object. After creating this object, I want to give it back to the Model class for further use. I can give primitive types back, but I'm unable to give any objects back. Is there a way to do this? =20 Kind regards, Jantien Sessink =20 |
|
From: Peter C. M. <pcm...@em...> - 2007-09-24 18:02:38
|
JPF uses normal Java reflection to call the NativePeer methods, so =20 the NativePeer has to be a public class, and the native methods have =20 to be "public static..". Please also note that you need to mange the =20 name (parameter/return type) if you have overloaded native methods. =20 The name mangling follows JNI and is documented on the web site -- Peter On Sep 24, 2007, at 12:42 AM, Jantien Sessink wrote: > Hi, > > Currently I'm looking at the possibility of using Java PathFinder =20 > for a research project. I=92m testing to run the main class in JPF =20 > and some other functions in the host JVM by creating a Model class =20 > and a NavtivePeer class. Both classes are printed below, as is the =20 > JPF output. When I try to run them in JPF, I get an =20 > IllegalAccessException. For some reason, the Model class can=92t find =20= > the functions defined in the NativePeer class. Is there something I =20= > forgot to do in order to let the model class see the NativePeer class? > > I hope you can help me with my problem. |
|
From: Flavio L. <fl...@gm...> - 2007-09-24 14:16:32
|
Hi Jantien,
I think the problem is that the class is defined with default visibility.
If you add "public" to the definition of your peer class things might work.
-Flavio
On 9/24/07, Jantien Sessink <jan...@gx...> wrote:
>
>
>
>
> Hi,
>
>
>
> Currently I'm looking at the possibility of using Java PathFinder for a
> research project. I'm testing to run the main class in JPF and some other
> functions in the host JVM by creating a Model class and a NavtivePeer class.
> Both classes are printed below, as is the JPF output. When I try to run them
> in JPF, I get an IllegalAccessException. For some reason, the Model class
> can't find the functions defined in the NativePeer class. Is there something
> I forgot to do in order to let the model class see the NativePeer class?
>
> I hope you can help me with my problem.
>
>
>
> Kind regards,
>
> Jantien Sessink
>
>
>
>
>
> -----------------------Model
> class------------------------------------------------------
>
> package nl.gx.firsthop;
>
>
>
> public class Test {
>
>
>
> public static void main(String[] args) {
>
> Integer test = 0;
>
> System.out.println("test = " + test.toString());
>
>
>
> test = increase(test, 10);
>
> System.out.println("test = " + test.toString());
>
>
>
> test = decrease(test, 10);
>
> System.out.println("test = " + test.toString());
>
> }
>
>
>
> native static int increase(Integer t, int increase);
>
>
>
> native static int decrease(Integer t, int decrease);
>
> }
>
> ----------------------------------------------------------------------------------------
>
>
>
> -----------------------NativePeer
> class-------------------------------------------------
>
> package nl.gx.firsthop;
>
>
>
> import gov.nasa.jpf.jvm.MJIEnv;
>
>
>
> class JPF_nl_gx_firsthop_Test {
>
>
>
> public static int increase (MJIEnv env, int rcls, int rInteger0, int
> v1) {
>
> System.out.println("Increasing test.....");
>
> for(int i = 0; i < v1; i++){
>
> rInteger0++;
>
> }
>
> return rInteger0;
>
> }
>
>
>
> public static int decrease (MJIEnv env, int rcls, int rInteger0, int
> v1) {
>
> System.out.println("Decreasing test.....");
>
> for(int i = 0; i < v1; i++){
>
> rInteger0--;
>
> }
>
> return rInteger0;
>
> }
>
>
>
> }
>
> ----------------------------------------------------------------------------------------
>
>
>
> -----------------------JPF
> output-------------------------------------------------------
>
> JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
>
>
>
>
>
> ======================================================
> system under test
>
> application: nl.gx.firsthop.Test.class
>
>
>
> ======================================================
> search started: 9/24/07 8:54 AM
>
> test = 0
>
>
>
> ======================================================
> error #1
>
> gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
>
> java.lang.IllegalAccessException: calling
> nl.gx.firsthop.Test.increase
>
> at nl.gx.firsthop.Test.increase(Native Method)
>
> at nl.gx.firsthop.Test.main(Test.java:9)
>
>
>
>
>
> ======================================================
> trace #1
>
> ------------------------------------------------------
> transition #0 thread: 0
>
> gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
>
>
>
> ======================================================
> snapshot #1
>
> no live threads
>
>
>
> ======================================================
> results
>
> error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
> "java.lang.IllegalAccessException: calling nl.gx.fi..."
>
>
>
> ======================================================
> search finished: 9/24/07 8:54 AM
>
> ----------------------------------------------------------------------------------------
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2005.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>
>
--
Google Talk: fl...@gm...
MSN Messenger: fl...@gm...
Skype: flerda
|
|
From: Jantien S. <jan...@gx...> - 2007-09-24 07:42:19
|
Hi,
=20
Currently I'm looking at the possibility of using Java PathFinder for a
research project. I'm testing to run the main class in JPF and some
other functions in the host JVM by creating a Model class and a
NavtivePeer class. Both classes are printed below, as is the JPF output.
When I try to run them in JPF, I get an IllegalAccessException. For some
reason, the Model class can't find the functions defined in the
NativePeer class. Is there something I forgot to do in order to let the
model class see the NativePeer class?
I hope you can help me with my problem.
=20
Kind regards,
Jantien Sessink
=20
=20
-----------------------Model
class------------------------------------------------------
package nl.gx.firsthop;
=20
public class Test {
=20
public static void main(String[] args) {
Integer test =3D 0;
System.out.println("test =3D " + test.toString());
=20
test =3D increase(test, 10);
System.out.println("test =3D " + test.toString());
=20
test =3D decrease(test, 10);
System.out.println("test =3D " + test.toString());
}
=20
native static int increase(Integer t, int increase);
=20
native static int decrease(Integer t, int decrease);
}
------------------------------------------------------------------------
----------------
=20
-----------------------NativePeer
class-------------------------------------------------
package nl.gx.firsthop;
=20
import gov.nasa.jpf.jvm.MJIEnv;
=20
class JPF_nl_gx_firsthop_Test {
=20
public static int increase (MJIEnv env, int rcls, int rInteger0,
int v1) {
System.out.println("Increasing test.....");
for(int i =3D 0; i < v1; i++){
rInteger0++;
}
return rInteger0;
}
=20
public static int decrease (MJIEnv env, int rcls, int rInteger0,
int v1) {
System.out.println("Decreasing test.....");
for(int i =3D 0; i < v1; i++){
rInteger0--;
}
return rInteger0;
}
=20
}
------------------------------------------------------------------------
----------------
=20
-----------------------JPF
output-------------------------------------------------------
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
=20
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D system under test
application: nl.gx.firsthop.Test.class
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search started:
9/24/07 8:54 AM
test =3D 0
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.IllegalAccessException: calling nl.gx.firsthop.Test.increase
at nl.gx.firsthop.Test.increase(Native Method)
at nl.gx.firsthop.Test.main(Test.java:9)
=20
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D trace #1
------------------------------------------------------ transition #0
thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D snapshot #1
no live threads
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
"java.lang.IllegalAccessException: calling nl.gx.fi..."
=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D search finished:
9/24/07 8:54 AM
------------------------------------------------------------------------
----------------
|
|
From: Qiang Z. <qz...@cs...> - 2007-09-18 17:08:31
|
Hi, I am new to the javapathfinder. I checked out the source from SourceForge.net and tried to build it. I did the following, svn checkout https://javapathfinder.svn.sourceforge.net/svnroot/javapathfinder/trunk under the trunk directory, I ran: java RunAnt run-tests but the compilation failed and I attached the error msg below. I just use the Ant and JUnit coming along with the source, so I suppose that there is nothing to configure, and the compilation should go through as expected, but now it failed. I wanna know what configuration I have to modify or what else I have to do. Thanks. ;=========================================================================== Compilation error msg ;=========================================================================== Buildfile: build.xml init: [mkdir] Created dir: /v/filer4b/projects-browne/uvv-fall2007/trunk/build [mkdir] Created dir: /v/filer4b/projects-browne/uvv-fall2007/trunk/build/jpf [mkdir] Created dir: /v/filer4b/projects-browne/uvv-fall2007/trunk/build/test [mkdir] Created dir: /v/filer4b/projects-browne/uvv-fall2007/trunk/build/env [mkdir] Created dir: /v/filer4b/projects-browne/uvv-fall2007/trunk/build/env/jvm [mkdir] Created dir: /v/filer4b/projects-browne/uvv-fall2007/trunk/build/env/jpf compile-jpf: [javac] Compiling 499 source files to /v/filer4b/projects-browne/uvv-fall2007/trunk/build/jpf [javac] /v/filer4b/projects-browne/uvv-fall2007/trunk/src/gov/nasa/jpf/tools/MethodTester.java:37: cannot find symbol [javac] symbol : class Test [javac] location: package gov.nasa.jpf [javac] import gov.nasa.jpf.Test; [javac] ^ [javac] /v/filer4b/projects-browne/uvv-fall2007/trunk/src/gov/nasa/jpf/jvm/MJIEnv.java:925: cannot find symbol [javac] symbol : variable JPF_java_lang_reflect_Method [javac] location: class gov.nasa.jpf.jvm.MJIEnv [javac] return JPF_java_lang_reflect_Method.getMethodInfo(this, mthRef); [javac] ^ [javac] hibounds=java.lang.Object [javac] hibounds=java.lang.Object [javac] /v/filer4b/projects-browne/uvv-fall2007/trunk/src/gov/nasa/jpf/tools/MethodTester.java:471: cannot find symbol [javac] symbol : class Test [javac] location: class gov.nasa.jpf.tools.MethodTester [javac] Test t = m.getAnnotation(Test.class); [javac] ^ [javac] /v/filer4b/projects-browne/uvv-fall2007/trunk/src/gov/nasa/jpf/tools/MethodTester.java:471: cannot find symbol [javac] symbol : class Test [javac] location: class gov.nasa.jpf.tools.MethodTester [javac] Test t = m.getAnnotation(Test.class); [javac] ^ [javac] Note: Some input files use unchecked or unsafe operations. [javac] Note: Recompile with -Xlint:unchecked for details. [javac] 4 errors BUILD FAILED /v/filer4b/projects-browne/uvv-fall2007/trunk/build.xml:151: Compile failed; see the compiler error output for details. Total time: 6 seconds |
|
From: yanjun.wen <yan...@gm...> - 2007-09-11 03:35:50
|
aGkgYWxsLA0KDQpXaGVuIEkgY29tcGlsZSBqcGYsIGFuIGVycm9yIGlzIGVuY291bnRlcmVkOg0K DQotLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0NCkU6XFByb2dyYW1pbmdcanBmXHRydW5r PmJ1aWxkLXRvb2xzXGJpblxhbnQgcnVuLXRlc3RzDQpCdWlsZGZpbGU6IGJ1aWxkLnhtbA0KDQpp bml0Og0KDQpjb21waWxlLWpwZjoNCiAgICBbamF2YWNdIENvbXBpbGluZyA0OTggc291cmNlIGZp bGVzIHRvIEU6XFByb2dyYW1pbmdcanBmXHRydW5rXGJ1aWxkXGpwZg0KICAgIFtqYXZhY10gRTpc UHJvZ3JhbWluZ1xqcGZcdHJ1bmtcc3JjXGdvdlxuYXNhXGpwZlx0b29sc1xNZXRob2RUZXN0ZXIu amF2YTozNzoNCiDV0rK7tb23+7rFDQogICAgW2phdmFjXSC3+7rFo7ogwOAgVGVzdA0KICAgIFtq YXZhY10gzrvWw6O6IMjtvP6w/CBnb3YubmFzYS5qcGYNCiAgICBbamF2YWNdIGltcG9ydCBnb3Yu bmFzYS5qcGYuVGVzdDsNCiAgICBbamF2YWNdICAgICAgICAgICAgICAgICAgICBeDQotLS0tLS0t LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0NCg0KSXQgc2VlbXMgdGhhdCBjbGFzcyBUZXN0IGNhbiBu b3QgYmUgZm91bmQuIEkgZmluZCB0aGUgc291cmNlIGZpbGUgVGVzdC5qYXZhIGluIHRydW5rXGFw cFxnb3ZcbmFzYVxqcGYuDQpXaGF0IHNob3VsZCBJIGRvIHRvIGZpeCB0aGUgcHJvYmxlbT8gDQoN ClRoYW5rcy4NCg0KDQoNCjIwMDctMDktMTEgDQoNCg0KDQp5YW5qdW4ud2VuIA0K |
|
From: Carlos P. <car...@gm...> - 2007-09-09 09:31:28
|
CarlosPita (car...@gm...) has invited you as a friend on Quechup... ...the social networking platform sweeping the globe Go to: http://quechup.com/join.php/aT0wMDAwMDAwMDA5OTgyMjQ3JmM9MTAyMjE0 to accept Carlos's invite You can use Quechup to meet new people, catch up with old friends, maintain a blog, share videos & photos, chat with other members, play games, and more. It's no wonder Quechup is fast becoming 'The Social Networking site to be on' Join Carlos and his friends today: http://quechup.com/join.php/aT0wMDAwMDAwMDA5OTgyMjQ3JmM9MTAyMjE0 ------------------------------------------------------------------ You received this because Carlos Pita (car...@gm...) knows and agreed to invite you. You will only receive one invitation from car...@gm.... Quechup will not spam or sell your email address, see our privacy policy - http://quechup.com/privacy.php Go to http://quechup.com/emailunsubscribe.php/ZW09amF2YXBhdGhmaW5kZXItdXNlckBsaXN0cy5zb3VyY2Vmb3JnZS5uZXQ%3D if you do not wish to receive any more emails from Quechup. ------------------------------------------------------------------ Copyright Quechup.com 2007. ------------------------------------ Go to http://quechup.com/emailunsubscribe.php/ZW09amF2YXBhdGhmaW5kZXItdXNlckBsaXN0cy5zb3VyY2Vmb3JnZS5uZXQ%3D if you do not wish to receive any more emails from Quechup |
|
From: harry h. <har...@ho...> - 2007-09-05 22:22:25
|
Hi,
I wrote a java Dining-Philosopher program and checked this program in the
JPF. JPF says there are no deadlocks but the program still suffers from
starvation. What is the best way to write the program so that there is no
starvation and is there a way to use JPF to check not only for freedom from
deadlock but also freedom from starvation?
The Philosopher class and the Fork class and the Mian class are provided as
below .
==============
public class Philosopher extends Thread {
private Fork left, right;
private int status, id;
private static final int IDLE = 0;
private static final int THINKING = 1;
private static final int HUNGRY = 2;
private static final int EATING = 3;
Philosopher(Fork l, Fork r, int an_id) {
left = l;
right = r;
id = an_id;
}
public void run() {
while (true) {
try {
think();
eat(left, right);
} catch (InterruptedException e) {
System.out.println(e);
}
}
}
public void think() {
status = THINKING;
status = HUNGRY;
}
public synchronized void eat(Fork l, Fork r) throws InterruptedException {
left.grab();
//add: release the left folk if right folk is inused
while (right.isInuse()) {
left.release(); --- l1
left.grab(); --- l2
}
right.grab(); --- l3
//ensure right and left folks are inused
assert (right.isInuse() && left.isInuse());
status = EATING;
System.out.println("PH " + id + " is eating");
left.release();
right.release();
status = IDLE;
System.out.println("PH " + id + " is idle");
}
}
================
public class Fork{
private boolean inuse;
// new added
private final ReentrantLock lock = new ReentrantLock(true);
public synchronized void grab() throws InterruptedException {
while (inuse) {
try {
wait();
} catch (InterruptedException e) {
System.out.println(e);
}
}
inuse = true;
}
public synchronized void release() throws InterruptedException {
inuse = false;
notify();
}
public boolean isInuse() {
return inuse;
}
}
============
public class DiningPhilosophers {
// The number of philosophers
public static final int COUNT = 3;
public static void main(String args[]) {
// Create the forks
Fork[] forks = new Fork[COUNT];
for (int i=0; i<COUNT; i++) {
System.out.println("Creating fork#: "+i);
forks[i]=new Fork();
}
// Create and start the Philosophers
Philosopher[] philosophers = new Philosopher[COUNT];
for (int i=0; i<COUNT; i++) {
System.out.println("Creating philosopher#: "+i);
philosophers[i]=new Philosopher(forks[i], forks[(i+1)%COUNT], i);
philosophers[i].start();
}
}
}
=============
Regards,
Hai
_________________________________________________________________
Share your special parenting moments!
http://www.reallivemoms.com?ocid=TXT_TAGHM&loc=us
|
|
From: David F. <da...@cs...> - 2007-08-21 13:15:47
|
Hello, Is there a way to make JPF model check temporal logic assertions? The original version of JPF supported LTL but then the support was dropped. What is the reason for not supporting temporal logic? How hard would it be to add such support? I found the following paragraph in the mailing list: From: Peter C. Mehlitz <pcmehlitz@em...> - 2005-07-12 16:33 ... One thing I had in mind for a while was using DynamicAssertions to do temporal stuff(i.e. turn part of the property into an JPF object, and use something like AspectJ to do the instrumentation), but there's no example for this yet. The other way to do temporal logic by means of the LTL2Buchi extension is not functional anymore - Dimitra's translator works fine, but the LTLSearch is certainly defunct (until somebody fixes it, hint, hint). Has anybody explored these tracks? has someone fixed LTLSearch? Thanks, David |
|
From: Armand N. <an...@pu...> - 2007-08-06 18:09:33
|
Is there any documentation regarding JPF-SE (http://ase.arc.nasa.gov/people/pcorina/papers/jpfseTACAS07.pdf)? The paper claims that a framework to perform symbolic execution has been added to the repository, but I can't find it or any documentation on how to use the symbolic engine. The paper says that it uses annotations in the form of method specifications. I am trying to find out what those annotations look like. Thanks, Armand |
|
From: John P. <jp...@go...> - 2007-08-02 23:26:22
|
That means you are hitting a method with native code, and JPF needs bytecode. You either need to stub out the code that is leading to this, or provide a java implementation for JPF to use via the Model Java Interface. There are examples - i think in the env directory. John On 8/2/07, doug arro <dou...@ya...> wrote: > > Hi, > > Has anyone any idea what would be causing this stack trace? > > ====================================================== error #1 > gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty > java.lang.UnsatisfiedLinkError: sun.misc.Signal.findSignal(Ljava/lang/String;)I > (no peer) > at sun.misc.Signal.<init>(Signal.java:123) > at java.lang.Terminator.setup(Terminator.java:40) > at java.lang.Shutdown.add(Shutdown.java:87) > at java.lang.Runtime.addShutdownHook(Runtime.java:190) > > > > Thanks. > > Doug > > ------------------------------ > Shape Yahoo! in your own image. Join our Network Research Panel today!<http://us.rd.yahoo.com/evt=48517/*http://surveylink.yahoo.com/gmrs/yahoo_panel_invite.asp?a=7> > > > ------------------------------------------------------------------------- > This SF.net email is sponsored by: Splunk Inc. > Still grepping through log files to find problems? Stop. > Now Search log events and configuration files using AJAX and a browser. > Download your FREE copy of Splunk now >> http://get.splunk.com/ > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > > |
|
From: doug a. <dou...@ya...> - 2007-08-02 23:04:31
|
Hi,
Has anyone any idea what would be causing this stack trace?
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: sun.misc.Signal.findSignal(Ljava/lang/String;)I (no peer)
at sun.misc.Signal.<init>(Signal.java:123)
at java.lang.Terminator.setup(Terminator.java:40)
at java.lang.Shutdown.add(Shutdown.java:87)
at java.lang.Runtime.addShutdownHook(Runtime.java:190)
Thanks.
Doug
---------------------------------
Shape Yahoo! in your own image. Join our Network Research Panel today! |
|
From: <ed...@uo...> - 2007-05-10 05:03:35
|
Hello,
I started to work on a project about PathFinder 3 months ago and I still have no results. If someone can give me some help it will be very useful because the project must be finish in 3 weeks.
I have the following function :
---[Code]---
private static void SampleCode(int a, int b, int c, int d) {
if(a>b) {
if (c>d)System.out.println("a>b and c>d");
else System.out.println("a>b and c<=d");
}
else {
if(c>d) System.out.println("a<=b and c>d");
else System.out.println("a<=b and c<=d");
}
return;
}
---[EndCode]---
The user choose 3 input groups : {a1,b1,c1,d1}, {a2,b2,c2,d2}, {a3,b3,c3,d3}
My program must :
* Execute the function with the group 1 et record the branchs taken (and display them)
* Execute the function with the group 2 :
- if the branch taken after the first IF Instruction is the same than for group 1, I need to record the position and go on with group 3
- else, continue the execution, record the branchs taken (and display them), stop the program
* Execute the function with the group 3 :
- if the branch taken after the first IF Instruction is different than for group 1, record the branchs taken (and display them), stop the program
- if it's the same than for group 1 :
- if the branch taken after the second IF Instruction is the same than for group 1, reload the group 2 and continue the execution with group 2
- else, continue the execution, record the branchs taken (and display them), stop the program
I really need your help because I really don't know what to do.
Thanks
Eric
|
|
From: Sergey K. <se...@cs...> - 2007-02-12 20:45:59
|
Hi Peter,
the option
> jpf.report.console.property_violation=error:trace:snapshot
is set on by default in my default.properties file, however only the last
transition is printed out, not the complete trace. Is there any other
option that I need to add to turn the trace on, or is the tracing not
completely implemented as yet.
thanks
sergey
On Mon, 12 Feb 2007, Peter C. Mehlitz wrote:
> Sergey,
>
> just add "trace" to the list of "property_violation" publisher topics, as in
>
> jpf.report.console.property_violation=error:trace:snapshot
>
> There are a bunch of "show_X" options that can be used to control the amount
> of info that goes into a trace. The "toXML" is pretty much superseded by the
> XML publisher (but that one isn't yet updated to the new publishing scheme).
>
> I will add some docu about the reporting system shortly.
>
> -- Peter
>
> On Feb 12, 2007, at 9:36 AM, Sergey Kulikov wrote:
>> Hi,
>>
>> I have a question, there is no more 'path to error' output, and I also saw
>> in the code that the 'toXML' feature was commented out (which printed the
>> same path to error in an xml file).
>>
>> Just wondering if there's going to be another way of reporting the path to
>> error?
>>
>> thanks
>> sergey
>
|
|
From: Peter C. M. <pcm...@em...> - 2007-02-12 18:29:26
|
Sergey, just add "trace" to the list of "property_violation" publisher topics, as in jpf.report.console.property_violation=error:trace:snapshot There are a bunch of "show_X" options that can be used to control the amount of info that goes into a trace. The "toXML" is pretty much superseded by the XML publisher (but that one isn't yet updated to the new publishing scheme). I will add some docu about the reporting system shortly. -- Peter On Feb 12, 2007, at 9:36 AM, Sergey Kulikov wrote: > Hi, > > I have a question, there is no more 'path to error' output, and I > also saw in the code that the 'toXML' feature was commented out > (which printed the same path to error in an xml file). > > Just wondering if there's going to be another way of reporting the > path to error? > > thanks > sergey |
|
From: Rayna A. <sa...@ma...> - 2007-02-03 11:39:15
|
Hi, Economize 50% on your medication with our site. http://www.zonrx.%com Impotant: Remove "%" to make the link working. -- Yeah, said Harry, glad that Cedric had made the suggestion rather than him. They pulled out their wands. Harry kept looking around him. He had, yet |
|
From: Melany M. <wor...@ca...> - 2007-01-24 10:05:16
|
Good day, VlA_AGRA $1, 80 ClA_ALIS $3, 00 LEV_VlTRA $3, 35 http://www.printeryml*com ( Important ! Replace "*" with "." ) -- Youre not by any chance writing out a new order form, are you? said Mrs. Weasley shrewdly. You wouldnt be thinking of restarting Weasleys Wizard Wheezes, by any chance? |
|
From: Onni R. <noa...@sa...> - 2007-01-23 17:37:33
|
Good day, VlA_AGRA $1, 80 ClA_ALIS $3, 00 LEV_VlTRA $3, 35 http://www.printeryml*com ( Important ! Replace "*" with "." ) -- Harry, Ron, Seamus, Dean, and Neville changed into their dress robes up in their dormitory, all of them looking very self-conscious, but none as much as Ron, who surveyed himself in the long mirror in the corner with |
|
From: Peter C. M. <pcm...@em...> - 2007-01-11 00:14:05
|
Hi Carlos,
Willem already mentioned this - we have the same requirements with the
UML state chart model checking, where we want to store every UML step as
a JPF state, but still do state matching. We are still experimenting
with this, but you can do it with ChoiceGenerators. Look at the
extensions/statechart/env/jpf/StateMachine.run() (which is kind of a
template method) and the getEnablingEvents() method in it's native peer
(which is the state storage point). This works because the only
condition that's used to determine transition boundaries is if executing
an instruction causes a new ChoiceGenerator to be registered in the
SystemState. What looks a bit weird is that you might get some
degenerated ChoiceGenerators that only exist for state storage purposes,
i.e. don't really produce choices (e.g. the
gov.nasa.jpf.jvm.choice.sc.NullSCEventGenerator), but that's in general
fine with specialized CG's where you obtain and process the choices
explicitly in your code. Generic things like ThreadChoiceGenerators
would be different of course.
With respect to your second question, it depends on how complex your
state extension is, and whether it involves executing its own code or
just consists of simple data. If it can be reduced to scalar values
(builtin types) then it's probably best to go with Willem's suggestion -
store it as field values into a JPF object, and get the state
storage/matching/restoration for free. If it gets complex (e.g. graphs),
and you don't want to create tons of JPF objects that actually might
blow up your JPF state space (which you nowadays can also filter of
course), then you might consider doing it like
gov.nasa.jpf.util.script.EventGeneratorFactory, i.e. use the JPF state
id to store/restore your extensions from a SearchListener. I'm not sure
if the EventGeneratorFactory is such a good example when to use this,
but it should at least show you how to use it.
-- Peter
Carlos Pita wrote:
> 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
>
> -------------------------------------------------------------------------
> 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
>
|
|
From: John M. <jo...@cs...> - 2007-01-08 11:25:33
|
Thanks to everyone who helped me getting Javapathfinder installed for
the first time on Linux; it works fine with:
$ ls
HelloWorld.class HelloWorld.java
$ jpf HelloWorld
... sensible output
One minor comment, though; if I try this instead, I see:
$ jpf HelloWorld.class
[SEVERE] JPF exception, terminating: could not load class
HelloWorld.class
gov.nasa.jpf.JPFException: could not load class HelloWorld.class
at gov.nasa.jpf.jvm.ClassInfo.getClassInfo(ClassInfo.java:408)
at gov.nasa.jpf.jvm.JVM.registerStartupClasses(JVM.java:333)
at gov.nasa.jpf.jvm.JVM.initialize(JVM.java:214)
at gov.nasa.jpf.JPF.run(JPF.java:367)
at gov.nasa.jpf.JPF.main(JPF.java:299)
$
A less confusing error message would be welcomed.
John A. Murdie
Department of Computer Science
University of York
UK
|
68 messages has been excluded from this view by a project administrator.
