Problem installing jpf-symbc

664 views
Skip to first unread message

German Vidal

unread,
Jul 31, 2014, 6:09:43 AM7/31/14
to java-pa...@googlegroups.com
Hi,

I was able to install jpf-core (on both linux and Mac OS mavericks) without problems, but I can't install jpf-symbc in any of these environments (though I did a year ago). 
I always get a large list of errors starting with

-compile-main:
    [javac] Compiling 266 source files to /home/gvidal/jpf/jpf-symbc/build/main
    [javac] warning: [options] bootstrap class path not set in conjunction with -source 1.6
    [javac] /home/gvidal/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:3: error: cannot find symbol
    [javac] import gov.nasa.jpf.ListenerAdapter;
    [javac]                    ^
    [javac]   symbol:   class ListenerAdapter
    [javac]   location: package gov.nasa.jpf
    [javac] /home/gvidal/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:4: error: package gov.nasa.jpf.search does not exist
    [javac] import gov.nasa.jpf.search.Search;
    [javac]                           ^
    ...

I installed jpf-core v6 instead, but I get the same error when compiling jpf-symbc. 

I also tried with both java 1.6 and 1.7, but always get similar results. The error listing above was using Java 1.7. With Java 1.6, I get

-compile-main:
    [javac] Compiling 266 source files to /home/gvidal/jpf/jpf-symbc/build/main
    [javac] /home/gvidal/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:3: cannot find symbol
    [javac] symbol  : class ListenerAdapter
    [javac] location: package gov.nasa.jpf
    [javac] import gov.nasa.jpf.ListenerAdapter;
    [javac]                    ^
    [javac] /home/gvidal/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:4: package gov.nasa.jpf.search does not exist
    [javac] import gov.nasa.jpf.search.Search;
    [javac]                           ^
    [javac] /home/gvidal/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:7: cannot find symbol
    [javac] symbol: class ListenerAdapter
    [javac] public class GreenListener extends ListenerAdapter {
    [javac]                                    ^
    ...

Any help to make jpf-symbc work would be greatly appreciated!

Best, German

Kasper Søe Luckow

unread,
Jul 31, 2014, 6:49:08 AM7/31/14
to java-pa...@googlegroups.com
Hi,
Did you correctly specify the location of jpf-core in the site.properties file? It should say something like:
jpf-core = /path/to/jpf-core
jpf-symbc = /path/to/jpf-symbc
extensions=${jpf-core},${jpf-symbc}

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.

German Vidal

unread,
Jul 31, 2014, 4:19:55 PM7/31/14
to java-pa...@googlegroups.com
Yes, thanks, I think so. This is my project tree:

/home/gvidal/jpf
/home/gvidal/jpf/jpf-core
/home/gvidal/jpf/jpf-symbc
/home/gvidal/jpf/jpf-shell

and this are the contents of /home/gvidal/.jpf/site.properties:

# JPF site configuration
jpf-core = /Users/gvidal/jpf/jpf-core

# symbolic extension
jpf-symbc= /Users/gvidal/jpf/jpf-symbc

# shell
jpf-shell = /Users/gvidal/jpf/jpf-shell

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

This is basically the same config I used last year and jpf-symbc compiled ok. The main difference now is moving from Java 1.6 to 1.7 (though I couldn't make it work even with Java 1.6) and using Apache ant instead of jpf-symbc/bin/ant..

Any other hint? Perhaps some environment variable I need to set? These are the ones I set:

$ echo $JAVA_HOME
/usr/lib/jvm/java-1.7.0-openjdk-1.7.0.65.x86_64
$ echo $ANT_HOME
/usr/local/ant

and this is the Java version I'm using:
$ java -version
java version "1.7.0_65"
OpenJDK Runtime Environment (rhel-2.5.1.2.el6_5-x86_64 u65-b17)
OpenJDK 64-Bit Server VM (build 24.65-b04, mixed mode)

Thanks!

German

Kasper Søe Luckow

unread,
Jul 31, 2014, 6:11:54 PM7/31/14
to java-pa...@googlegroups.com
This is not related to the JDK you are using - it is classpath issue.
It confuses me a bit that you initially provided a unix project tree (/home/...) including the path to the site.properties file, but site.properties seems to be specifying paths usually found in a mac os x directory structure (/Users/...). My guess is that the paths are not correct in the file.

Kasper

German Vidal

unread,
Jul 31, 2014, 6:55:17 PM7/31/14
to java-pa...@googlegroups.com
Oops, sorry, I pasted the wrong file (I'm connecting to the linux server remotely and choosed the wrong window). The right file is:


# JPF site configuration
jpf-core=/home/gvidal/jpf/jpf-core

# symbolic extension
jpf-symbc=/home/gvidal/jpf/jpf-symbc

# shell
jpf-shell=/home/gvidal/jpf/jpf-shell

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

which should be ok. I even tried deleting the site.properties file (since, according to the build.xml file, the default directory is "../jpf-core", which is right), but it didn't work either.

What puzzles me is that I'm having the same issue in both my laptop (Mac OS Mavericks) and an old linux server (running Red Hat). In either case I get the same errors. For some reason, it can't find the jpf-core classes when compiling either jpf-symbc or jpf-shell. E.g., the first error in my previous post referred to ListernerAdapter, which is here:

/home/gvidal/jpf/jpf-core/build/main/gov/nasa/jpf/ListenerAdapter.class

(where it should be). So I agree, it seems it is classpath problem, but I have no idea where the problem is. Any further suggestion will be welcome!

German

Quoc-Sang Phan

unread,
Jul 31, 2014, 7:36:57 PM7/31/14
to java-pa...@googlegroups.com
Hi,

Could you verify that there is a file called "jpf.jar" under the following path:

/home/gvidal/jpf/jpf-core/build/jpf.jar

If the file does not exist, then you need to build the core before building jpf-symbc.

Sang

German Vidal

unread,
Jul 31, 2014, 7:45:02 PM7/31/14
to java-pa...@googlegroups.com
Yes, it is. Actually, I got no significant errors from compiling jpf-core (only some warnings). These are the contents of jpf-core/build:


annotations
classes
classloader_specific_tests.jar
examples
jpf-annotations.jar
jpf-classes.jar
jpf.jar
main
peers
RunJPF.jar
RunTest.jar
tests

German 

Quoc-Sang Phan

unread,
Aug 1, 2014, 2:59:40 AM8/1/14
to java-pa...@googlegroups.com
Hi,

Obviously, there is some problem with the classpath settings in build.xml, but I'm not very familiar with Ant.

I write simple scripts for you to build jpf-symbc, using simple javac.

You need to modify the path to junit-4.XX.jar in compile.sh, then run build.sh to compile and create the jar files.

Sang
build.sh
compile.sh

German Vidal

unread,
Aug 1, 2014, 4:37:09 AM8/1/14
to java-pa...@googlegroups.com
Many thanks! In principle, it seems that your script does the trick and compiles jpf-symbc ok (I only get some warnings like "Reflection is internal proprietary API and may be removed in a future release").

However, it still fails. If I try, e.g., this:

  jpf-symbc$ bin/jpf src/examples/NumberExample.jpf 

I get:

@@@@ key=vm.attributors
[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo for entry "vm.classloader.class":
> exception in gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo(gov.nasa.jpf.vm.VM,int):
>> java.lang.NullPointerException
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

Perhaps the compilation process was not fine after all? How could I check it?


German

Quoc-Sang Phan

unread,
Aug 1, 2014, 7:18:17 AM8/1/14
to java-pa...@googlegroups.com
Could you try to run jpf-core/bin/jpf? because it runs the RunJPF.jar that you compiled from the core.

The script jpf-symbc/bin/jpf runs RunJPF.jar under jpf-symbc/tools, and the file could be outdated.

If it still fails, could you also try to add to the NumberExample.jpf the path to site.properties as follows:

site=path/to/the/file/site.properties

Sang

German Vidal

unread,
Aug 1, 2014, 10:18:43 AM8/1/14
to java-pa...@googlegroups.com
Same results either way. Actually I have /home/gvidal/jpf/jpf-core/bin in my PATH and thus this is the one I always use.
But, for some reason, it can't find the class gov.nasa.jpf.symbc.SymbolicInstructionFactory. This is perhaps the way
I compiled the project? (rather than using ant and build.xml I mean)

German

Kasper Søe Luckow

unread,
Aug 1, 2014, 10:23:30 AM8/1/14
to java-pa...@googlegroups.com
This is not related to how you compiled - it is still a classpath issue, which you will need to fix. You can try running RunJPF.jar and set the classpath correctly (using -classpath) to the jpf-symbc classes.

German Vidal

unread,
Aug 1, 2014, 10:46:15 AM8/1/14
to java-pa...@googlegroups.com
Oops, I'm not that sure. I have checked it and I've found that the contents of jpf-symbc/build/examples are identical to those in jpf-core/build/examples (and the same happens with jpf-symbc/build/main/gov/... and jpf-core/build/main/gov...)

So I think the scripts build.sh and compile.sh are basically compiling jpf-core into jpf-symbc/build, which is not what was intended. Perhaps I'm missing something?

German

Kasper Søe Luckow

unread,
Aug 1, 2014, 10:57:30 AM8/1/14
to java-pa...@googlegroups.com
You should figure out why you cannot make a proper build using the provided ant builds - this could probably solve both problems. My guess is that the paths of jpf-core and jpf-symbc ant properties are not correct (or are not read).

German Vidal

unread,
Aug 1, 2014, 12:03:05 PM8/1/14
to java-pa...@googlegroups.com
Ok, thanks. 

Anyway, I'm now re-checking the errors. The first one, for instance is this:

    [javac] /home/gvidal/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java:41: error: cannot find symbol

    [javac] import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;

And I've looked for InvokeInstruction, and it's in a different location:

   /home/gvidal/jpf/jpf-core/build/main/gov/nasa/jpf/vm/bytecode/InvokeInstruction.class

(so the correct import would be import gov.nasa.jpf.jpf.vm.bytecode.InvokeInstruction; )

So it seems to me that the files in the jpf-symbc project are not compatible with the last version of jpf-core after all...

German

German Vidal

unread,
Aug 1, 2014, 1:01:45 PM8/1/14
to java-pa...@googlegroups.com
Here:

  (so the correct import would be import gov.nasa.jpf.jpf.vm.bytecode.InvokeInstruction; )

I meant:

  (so the correct import would be import gov.nasa.jpf.vm.bytecode.InvokeInstruction; )

Anyway, now I have tried v6 of both jpf-core and jpf-symbc, and everything compiles ok with JDK 1.6 (also for jpf-shell).

So, as I said, my impression is that the current jpf-symbc project in the repository is not compatible with the current jpf-core. One should consider v6 for them to work fine...

Thank you all for your help!

German

German Vidal

unread,
Aug 1, 2014, 1:56:10 PM8/1/14
to java-pa...@googlegroups.com
Last update: I compiled v6 also with Java 1.7 too. Everything's fine.

German

Quoc-Sang Phan

unread,
Aug 1, 2014, 6:29:37 PM8/1/14
to java-pa...@googlegroups.com
Hi,

Sorry, I made a mistake in the script I sent you. I put an unnecessary cd command, and it jumped to jpf-core to compile.

Could you try the new script in attachment? Please edit the path to junit-4.XX.jar in compile.sh, and then run ./build.sh?

I have checked the content of the output folders and jar files. This script should work, and compile jpf-symbc correctly (at least in my machine :-) ).

Sang
compile.sh

German Vidal

unread,
Aug 1, 2014, 6:41:39 PM8/1/14
to java-pa...@googlegroups.com
Thanks Sang! But, as I mentioned in a previous post, even if the script works fine, the problem is that the current version of jpf-symbc seems to be inconsistent with the current version of jpf-core. Finally I have tried with the v6 versions of both projects and they compiled ok (using bin/ant).

German

Quoc-Sang Phan

unread,
Aug 2, 2014, 2:18:00 AM8/2/14
to java-pa...@googlegroups.com
Hi German,

I have just pulled the latest version of jpf-core, and the latest version of jpf-symbc.
They are compatible, and can be compiled without errors.

Could you try pulling again?

Sang

German Vidal

unread,
Aug 2, 2014, 5:31:51 AM8/2/14
to java-pa...@googlegroups.com
Hi Sang, I've used these versions and they compile ok. Many thanks for your help!

German
Reply all
Reply to author
Forward
0 new messages