Modeling a method

[Ivan]

Hi,

TL; DR: Is it possible to model only one method of the class?

Full story:

I'm trying to verify a program that executes external process using Runtime.exec() and then Process.waitFor() etc.

As I understand it, jpf-core cannot do it, since it encounters native ProcessEnvironment.environ() somewhere inside the exec() methods.

The thing is I don't really need the results of the external execution, so any dummy implementation of the Runtime.exec() will work for me.

I have tried jpf-nhandler, but both delegating and skipping won't work: delegating results in the NullPointerException down the line in OTF_JPF_java_lang_UNIXProcess.forkAndExec() 

(I assume this is because it's a system-specific method?) and just skipping returns a null value that is later causing exception, when SUT calls Process.waitFor().

So what I want to do is to create a dummy method that will not cause any exceptions.

I have added the following Runtime.java to the java.lang package in jpf-core/classes:

package java.lang;

import java.io.IOException;

public class Runtime {

    public Process exec(String command) throws IOException {

        return new ProcessBuilder().start();

    }

}

But this causes the rest of the Runtime.* methods to fail in JPF:

java.lang.Error: Unresolved compilation problems: 

The method getRuntime() is undefined for the type Runtime

The method freeMemory() is undefined for the type Runtime

The method gc() is undefined for the type Runtime

The method freeMemory() is undefined for the type Runtime

at gov.nasa.jpf.JPF.run(JPF.java:604)

at gov.nasa.jpf.JPF.start(JPF.java:190)

at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)

at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)

at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)

at java.lang.reflect.Method.invoke(Method.java:606)

at gov.nasa.jpf.tool.Run.call(Run.java:76)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)

1. Is there any way I can model only one method in Runtime without having to model others? 

2. Am I on the right track with the exec() method implementation?

Any hint at all on how to verify a SUT with Runtime.exec() would be appreciated.

Thanks.

[PETER C MEHLITZ]

you should use a NativePeer for this, not a model class. NativePeers can override single methods with native (host VM side) executed code, and if you ever want to really execute an external process you would need a native Runtime.exec() anyways. However, what you need to model (on the JPF executed side) is java.lang.Process

-- Peter

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.