Running SPF from command line

[Teodoro Filippini]

Hello everyone.

I've been trying to run SPF on OS X's terminal. I installed JPF fine, modified the site.properties file, etc... Following the official website's instructions verbatim.

I was going on to try and run SPF, following the website's instructions, however they are incomplete and ambiguous:

"

• Here is an example of a JPF run configuration (Example.jpf). It enables symbolic execution of method "test" in main class Example.java, where first argument is symbolic, and second argument is concrete.

"

1) How do I run this? I didn't even try, I don't know where to place it and what to call in order to run it. Besides, there is no method called "test" in the Example.java class.

2) How do I run anything with SPF? I tried

java -jar tools/RunJPF.jar src/examples/Assume.jpf

obtaining

error: cannot find gov.nasa.jpf.JPF

And here are more runs (basically guessing the syntax for SPF), with the error outputs I got:

jona:JPF-files TF$ java -jar jpf-core/build/RunJPF.jar Example.jpf

[SEVERE] JPF configuration error: class not found gov.nasa.jpf.symbc.SymbolicListener

[SEVERE] JPF terminated

jona:JPF-files TF$ java -jar jpf-core/build/RunJPF.jar jpf-symbc/src/examples/AssertionLifting.jpf

[WARNING] unknown classpath element: /Users/TF/Desktop/JPF-files/$/Users/TF/Desktop/JPF-files/jpf-symbc/build/examples

[SEVERE] JPF configuration error: class not found .symbc.SymbolicListener

[SEVERE] JPF terminated

jona:JPF-files TF$ java -Djava.library.path=/Users/TF/Desktop/JPF-files/jpf-symbc/lib -jar /Users/TF/Desktop/JPF-files/jpf-core/build/RunJPF.jar /Users/TF/Desktop/JPF-files/jpf-symbc/ExSymExe.jpf

Exception in thread "main" ---------------------- JPF error stack trace ---------------------

JPF configuration error: error in /Users/TF/Desktop/JPF-files/jpf-core/jpf.properties : property file does not exist: /Users/TF/Desktop/JPF-files/jpf-symbc/ExSymExe.jpf

at gov.nasa.jpf.Config.exception(Config.java:1114)

at gov.nasa.jpf.Config.loadProperties(Config.java:424)

at gov.nasa.jpf.Config.<init>(Config.java:217)

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

jona:JPF-files TF$ java -Djava.library.path=/Users/TF/Desktop/JPF-files/jpf-symbc/lib -jar /Users/TF/Desktop/JPF-files/jpf-core/build/RunJPF.jar /Users/TF/Desktop/JPF-files/jpf-symbc/Example.jpf

[SEVERE] JPF configuration error: class not found gov.nasa.jpf.symbc.SymbolicListener

[SEVERE] JPF terminated

So... Does anyone know how to work with SPF from terminal?

Thanks,

Teodoro

[Quoc-Sang Phan]

Hi,

You should run the script jpf under jpf-core/bin, no matter what project, e.g. SPF, you are running.

Best wishes,

Sang

[Teodoro Filippini]

Thank you for your reply, Sang. I was reading your discussion of several years ago on the same topic, but couldn't find a solution.

I call the jpg script under jpg-core/bin, but I still get that the Listeners are not found, and the process is aborted:

[SEVERE] JPF configuration error: class not found .symbc.SymbolicListener

[SEVERE] JPF terminated

Could you provide me an example call that works for you from a terminal? E.g., running one of the examples in the jpf-symbc/src/examples/ folder. I tried

jpf-core/bin/jpf jpf-symbc/src/examples/Assume.jpf

obtaining the afore-mentioned error.

Thank you deeply,

Teodoro

[Teodoro Filippini]

Also, I noticed that in jpg-symbc/build the listeners are not built, i.e. there ar eno listener classes, opposite to the situation in jpg-core/. 

I wonder, how to fix the listener problem?

[Teodoro Filippini]

I guess I need to build jpf-symbc via "ant test" the same way I did for jpg-core (which works fine). I wonder why is this not written in the website's instructions...

Anyway, unfortunately the ant test itself fails. I've been trying to run "bin/ant test", as well as java -jar tools/RunAnt.jar test, 

but I get in both cases

ERROR: no ant.jar found in known tools dirs (check your site.properties)

The only thing that at least produces an output is the same I did for building jpf-core: cd to jpf-symbc and simply running "ant test". However, I still get an error:

BUILD FAILED

/Users/TF/Desktop/JPF-files/jpf-symbc/build.xml:118: Compile failed; see the compiler error output for details.

The output is a series of hundreds of "can't find symbol" like this:

  symbol:   class Instruction

  location: class SymbolicInstructionFactory

/Users/TF/Desktop/JPF-files/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java:373: error: cannot find symbol

          public Instruction l2d() {

For Instructions with various names: l2f(9, f2l(), f2i(), ...... 

So out of despair I tried "sudo ant test" and got no more errors, just warnings. However, the build failed:

compile:

-jar-jvm:

      [jar] Building jar: /Users/TF/Desktop/JPF-files/jpf-symbc/build/jpf-symbc.jar

-jar-jpf:

      [jar] Building jar: /Users/TF/Desktop/JPF-files/jpf-symbc/build/jpf-symbc-classes.jar

-jar-annotations:

      [jar] Building jar: /Users/TF/Desktop/JPF-files/jpf-symbc/build/jpf-symbc-annotations.jar

build:

test:

BUILD FAILED

/Users/TF/Desktop/JPF-files/jpf-symbc/build.xml:221: /Users/TF/Desktop/JPF-files/jpf-symbc/${junit.home} does not exist.

I wonder why is it searching for JUnit inside jpf-symbc.

If someone encountered these issues, let me know... I am well beyond trying random stuff at this point

[Kasper Søe Luckow]

Can you show us the contents of your ${HOME}/.jpf/site.properties file?

My guess is that you didn't add jpf-symbc to the list of extensions, like this:

extensions=${jpf-core},${jpf-symbc}

Alternatively, you can add in the jpf file for your SUT(s):

@using = jpf-symbc

You can run the regression tests with

$ ant test

Make sure that the JUNIT_HOME env variable is set.

- Kasper

--

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

[Teodoro Filippini]

Dear Kasper,

Thank you for answering.

I set up the site.properties file just as illustrated on the JPF website, also adding the jpf-symbc extension. I also set JUNIT_HOME to the folder in which I put the .jar of junit and hamcrest. It still doesn't see it; should I add JUNIT_HOME to the CLASSPATH?

I also tried modifying the build.xml file, explicitly putting the path to the JUNIT folder, and now the "ant test" is succesful; however, it fails every single test because it doesn't find the class util.gov....JPFtest. It must be some kind of classpath problem... 

---

Da: java-pa...@googlegroups.com <java-pa...@googlegroups.com> per conto di Kasper Søe Luckow <kslu...@gmail.com>
Inviato: giovedì 12 maggio 2016 19.11.09
A: Java™ Pathfinder
Oggetto: Re: [JPF] Re: Running SPF from command line

 

You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/fvYID669dII/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.

[Kasper Søe Luckow]

Yes, it is a classpath problem. Can you show us the site.properties file? Where is it located?

[Teodoro Filippini]

Dear Kasper,

The site.properties file, located in /Users/TF/.jpf , contains the following:

  

user.home = /Users/TF

jpf.home = ${user.home}/Desktop/JPF-files 

  

# can only expand system properties  

jpf-core = ${jpf.home}/jpf-core  

# symbolic extension  

jpf-symbc = ${jpf.home}/jpf-symbc 

extensions=${jpf-core},${jpf-symbc}  

and of course, this reflects its real position. After all, if it didn't for jpg-core, I wouldn't be able to successfully run ant test on it.

[Teodoro Filippini]

Dear all,

I solved my installation problems by forcefully adding to the CLASSPATH the directories of unfound files. Now SPF works, however during ant test I got one error:

gov.nasa.jpf.JPFNativePeerException: 

exception in native method java.lang.Object.clone
...
...

Caused by java.lang.IllegalAccessError: tried to access field 

gov.nasa.jpf.vm.ElementInfo.fields from class gov.nasa.jpf.vm.JPF_java_lang_Object

Should I worry about it?

P.S. I am currently writing a guide about all the problems I faced while installing SPF for bash use on OS X; I will share it here soon.