SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
124 stars 89 forks source link

Compile with Java 11 and update to gradle 8.4 #96

Open Ao-senXiong opened 3 months ago

sohah commented 3 months ago

Thank you @Ao-senXiong for your contributions. I have a couple of comments on this pull request:

  1. This pull request updates both the Java version and the gradle version. If you want to include changes to the gradle version in this pull request, then please change the description of the pull request, and also modify the ReadMe file to indicate the new version of both Java and gradle that we are updating this branch to.
  2. I observed that you've deleted some files from jpf-symbc/src/classes is this intentional? If yes, can you please explain the reason for that?
sohah commented 2 months ago

@Ao-senXiong , thank you for your contributions. Things look good to me. Here are some comments on the ReadMe

  1. I think the line where we are cloning the branch, should be pointing to the gradle-build-java-11.
  2. I do not think the warning after building jpf-core is valid anymore on this branch. I think it would be best if you ran that command on your machine and then update the readme with the console output that is being generated. The warnings are no longer valid now.
  3. Also I think you should be changing the output of the java -version for the system requirements
  4. The SPF example java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar ./src/examples/demo/NumericExample.jpf , does not run for me after I follow the steps in the readme. Have you looked into this? I am getting
    [SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class":
    > exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
    >> java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
    > used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
    [SEVERE] JPF terminated
Ao-senXiong commented 1 month ago

@Ao-senXiong , thank you for your contributions. Things look good to me. Here are some comments on the ReadMe

  1. I think the line where we are cloning the branch, should be pointing to the gradle-build-java-11.
  2. I do not think the warning after building jpf-core is valid anymore on this branch. I think it would be best if you ran that command on your machine and then update the readme with the console output that is being generated. The warnings are no longer valid now.
  3. Also I think you should be changing the output of the java -version for the system requirements
  4. The SPF example java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar ./src/examples/demo/NumericExample.jpf, does not run for me after I follow the steps in the readme. Have you looked into this? I am getting
[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class":
> exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
>> java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

I updated this PR with new build instructions for Java 11 https://github.com/SymbolicPathFinder/jpf-symbc/pull/96/files#diff-b335630551682c19a781afebcf4d07bf978fb1f8ac04c6bf87428ed5106870f5. Please review it when you have time. I did not update the docker section because I did not touch it yet. After merge deprecated API PR, I will update the README.md again with new installation message.

Ao-senXiong commented 1 month ago

The SPF example java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar ./src/examples/demo/NumericExample.jpf , does not run for me after I follow the steps in the readme. Have you looked into this? I am getting [SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class": exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):

java.lang.NoClassDefFoundError: sun/misc/SharedSecrets used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM [SEVERE] JPF terminated

My local works fine, are you using Java 11 and gradle 8.4? java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar ./src/examples/demo/NumericExample.jpf

symbolic.min_int=-2147483648 symbolic.min_long=-9223372036854775808 symbolic.min_short=-32768 symbolic.min_byte=-128 symbolic.min_char=0 symbolic.max_int=2147483647 symbolic.max_long=9223372036854775807 symbolic.max_short=32767 symbolic.max_byte=127 symbolic.max_char=65535 symbolic.min_double=4.9E-324 symbolic.max_double=1.7976931348623157E308 JavaPathfinder core system v8.0 (rev 387f330c31c56db8f645b4cb05239984179f1345) - (C) 2005-2014 United States Government. All rights reserved.

sohah commented 1 month ago

@Ao-senXiong , I am still seeing references to Java 8 and Gradle 6.9 in many occurrences in the ReadMe. Please fix all occurrences. Also for the docker section, you need to update it accordingly. This needs to be fixed/checked too.

Ao-senXiong commented 4 weeks ago

@Ao-senXiong , I am still seeing references to Java 8 and Gradle 6.9 in many occurrences in the ReadMe. Please fix all occurrences. Also for the docker section, you need to update it accordingly. This needs to be fixed/checked too.

Okay, thanks! I think some of the java 8 ocurrence was in the detailed instructions section and docker section. I have not touched the docker image for spf before. I guess we need to create new docker image for java 11...