Re: [Javapathfinder-user] About java.lang.UnsatisfiedLinkError

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

En,

you have basically two choices:

(1) add a File.list() implementation (which shoulnd't be too hard if  
you are only interested in the standard functionality) - but that  
might not be all that's required to make the sun.misc.* classes  
happy. The other thing is that our File class is supposed to be an  
abstraction (even though Owen wrote it mostly being interested in  
RandomAccessFile data state keeping, and File doesn't have a real  
purpose yet) - question is what we would model here (state tracked  
directory contents?) Of course, that would be our preferred choice :)

(2) try to find a cut point in java.security or sun.misc.Launcher,  
where you can cut off further sun.misc (and File) usage by a stub. If  
you are not interested in the java.security.* internals, that sounds  
feasible. That's probably your best shot.

-- Peter

On Sep 15, 2005, at 9:16 PM, En Ye wrote:


> Peter,
>
> Thank you very much for your advice.  After solving the
> "java.lang.UnsatisfiedLinkError" exception by adding native peer
> class, I reran the same program. Then I encountered a new exception as
> following:
>
> java.lang.NoSuchMethodException: java.io.File.list()
>     at sun.misc.Launcher$ExtClassLoader.getExtURLs(sun\misc 
> \Launcher.java:161)
>     at sun.misc.Launcher$ExtClassLoader.<init>(sun\misc 
> \Launcher.java:137)
>     at sun.misc.Launcher$1.run(sun\misc\Launcher.java:121)
>     at java.security.AccessController.doPrivileged(java\security 
> \AccessController.java:53)
>     at sun.misc.Launcher$ExtClassLoader.getExtClassLoader(sun\misc 
> \Launcher.java:118)
>     at sun.misc.Launcher.<init>(sun\misc\Launcher.java:51)
>     at sun.misc.Launcher.<clinit>(sun\misc\Launcher.java:39)
>     at java.security.Security.getEngineClassName(java\security 
> \Security.java:529)
>     at java.security.Security.getEngineClassName(java\security 
> \Security.java:595)
>     at java.security.Security.getImpl(java\security\Security.java: 
> 1044)
>     at java.security.KeyPairGenerator.getInstance(java\security 
> \KeyPairGenerator.java:146)
>     at DHKeyAgreement3.run(DHKeyAgreement3.java:54)
>     at DHKeyAgreement3.main(DHKeyAgreement3.java:38).
>
> I know the exception was thown because the File model class in the
> "javapathfinder\env\jpf\java\io" doesn't provide "list" function while
> the original File class does. So could you kindly tell me how can I
> solve this problem? It is seemly impossible to only add a stubbed
> "list" function to the File model class since the "list" function
> needs to return a String array. If I just delete the File model class,
> what will it affect the JavaPathFinder? Thanks in advance for your
> help.
>
> En
>
> On 9/6/05, Peter C. Mehlitz <pcm...@em...> wrote:
>
>
>> En,
>>
>> Yes, you are right - ObjectStream native methods are not supported
>> yet. It's probably better to intercept the BigInteger.<clinit> in a
>> native peer (like StringBuffer does too) than to fiddle directly with
>> the ObjectStreamClass, since I assume it really needs the native
>> methods. We don't support serialization yet, anyways.
>>
>> -- Peter
>>
>> On Sep 4, 2005, at 9:01 PM, En Ye wrote:
>>
>>
>>
>>> Hi all,
>>>
>>> When I used JavaPathFinder to verify a Java Class DHKeyAgreement3
>>> (source code is attached at the end). I encountered an exception
>>> listed below:
>>>
>>> java.lang.UnsatisfiedLinkError:
>>> java.io.ObjectStreamClass.initNative (no peer)
>>>     at java.io.ObjectStreamClass.<clinit>(java\io
>>> \ObjectStreamClass.java:133)
>>>     at java.io.ObjectStreamField.<init>(java\io
>>> \ObjectStreamField.java:71)
>>>     at java.io.ObjectStreamField.<init>(java\io
>>> \ObjectStreamField.java:45)
>>>     at java.math.BigInteger.<clinit>(java\math\BigInteger.java:3008)
>>>     at DHKeyAgreement3.<clinit>(DHKeyAgreement3.java:204)
>>>     at DHKeyAgreement3.main(DHKeyAgreement3.java:37)
>>> ..
>>> I guess the exception was thrown because the JPF cannot find an
>>> appropriate native peer class for java.io.ObjectStreamClass (JPF  
>>> don't
>>> provide this native peer class). If it is right, can I create a  
>>> native
>>> peer class for it to eliminate the exception? And if I can, can I do
>>> it as the following:
>>> (1) create a MJI model class for java.io.ObjectStreamClass and  
>>> put it
>>> in the env\jpf folder
>>> (2) use "GenPeer" to generate a native peer class for
>>> java.io.ObjectStreamClass and put in the env\jvm folder
>>> ?  Or it there any other solution? Is there any related  
>>> documentation
>>> on it? Thanks in advance for your help.
>>>
>>>
>>
>>
>>
>
>
>