diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 29682857..cd7a0e9f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -2,10 +2,10 @@ name: Gradle Package on: push: - branches: [ gradle-build ] + branches: [ gradle-build-java-11 ] pull_request: - branches: [ gradle-build ] + branches: [ gradle-build-java-11 ] workflow_dispatch: @@ -28,7 +28,7 @@ jobs: - name: Set up JDK 1.8 uses: actions/setup-java@v3 with: - java-version: 8 + java-version: 11 distribution: 'temurin' cache: gradle diff --git a/README.md b/README.md index ee288b96..6ca8dcb6 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ As of August 2022, we migrated our build workflow to `Gradle`. While migrating t ## Quick Start Guide -SPF requires: **Java 8** and **Gradle 6.9**. +SPF requires: **Java 11** and **Gradle 8.4**. ### 1. Get the latest SPF version ```{bash} @@ -72,7 +72,7 @@ Submodule path 'jpf-core': checked out '45a4450cd0bd1193df5419f7c9d9b89807d00db6 cd SPF gradle :jpf-core:buildJars ``` -If using a gradle version > 6.9, you can point gradle to the Java 8 home on your machine. You need to specify that for all gradle commands blow. For example: +If using a gradle version > 8.4, you can point gradle to the Java 11 home on your machine. You need to specify that for all gradle commands blow. For example: ```{bash} gradle :jpf-core:buildJars -Dorg.gradle.java.home=/usr/lib/jvm/java-8-openjdk-amd64 @@ -86,109 +86,23 @@ jpf-core jpf-symbc > Task :jpf-core:compileJava -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:21: warning: sun.misc.SharedSecrets is internal proprietary API and may be removed in a future release -import sun.misc.SharedSecrets; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:22: warning: sun.misc.JavaLangAccess is internal proprietary API and may be removed in a future release -import sun.misc.JavaLangAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:85: warning: sun.misc.JavaLangAccess is internal proprietary API and may be removed in a future release - static final JavaLangAccess JLA = SharedSecrets.getJavaLangAccess(); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:85: warning: sun.misc.SharedSecrets is internal proprietary API and may be removed in a future release - static final JavaLangAccess JLA = SharedSecrets.getJavaLangAccess(); - ^ -Note: /Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/choice/PermutationCG.java uses or overrides a deprecated API. -Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. -4 warnings - -> Task :jpf-core:compileClassesJava -/Users/yannic/Desktop/SPF/jpf-core/src/classes/java/lang/ClassLoader.java:29: warning: sun.misc.CompoundEnumeration is internal proprietary API and may be removed in a future release -import sun.misc.CompoundEnumeration; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/java/lang/ClassLoader.java:114: warning: sun.misc.CompoundEnumeration is internal proprietary API and may be removed in a future release - return new CompoundEnumeration(resEnum); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/JavaNetAccess.java:32: warning: sun.misc.URLClassPath is internal proprietary API and may be removed in a future release - URLClassPath getURLClassPath (URLClassLoader ucl); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:52: warning: sun.misc.JavaUtilJarAccess is internal proprietary API and may be removed in a future release - private static JavaUtilJarAccess javaUtilJarAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:60: warning: sun.misc.JavaOISAccess is internal proprietary API and may be removed in a future release - private static JavaOISAccess javaOISAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:61: warning: sun.misc.JavaObjectInputStreamAccess is internal proprietary API and may be removed in a future release - private static JavaObjectInputStreamAccess javaObjectInputStreamAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:82: warning: sun.misc.JavaUtilJarAccess is internal proprietary API and may be removed in a future release - public static JavaUtilJarAccess javaUtilJarAccess() { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:88: warning: sun.misc.JavaUtilJarAccess is internal proprietary API and may be removed in a future release - public static void setJavaUtilJarAccess(JavaUtilJarAccess access) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:142: warning: sun.misc.JavaObjectInputStreamAccess is internal proprietary API and may be removed in a future release - public static JavaObjectInputStreamAccess getJavaObjectInputStreamAccess() { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:151: warning: sun.misc.JavaObjectInputStreamAccess is internal proprietary API and may be removed in a future release - public static void setJavaObjectInputStreamAccess(JavaObjectInputStreamAccess access) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:162: warning: sun.misc.JavaOISAccess is internal proprietary API and may be removed in a future release - public static void setJavaOISAccess(JavaOISAccess access) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:166: warning: sun.misc.JavaOISAccess is internal proprietary API and may be removed in a future release - public static JavaOISAccess getJavaOISAccess() { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:175: warning: sun.misc.JavaObjectInputStreamReadString is internal proprietary API and may be removed in a future release - public void setJavaObjectInputStreamReadString(sun.misc.JavaObjectInputStreamReadString ignored) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/java/lang/System.java:64: warning: sun.misc.VM is internal proprietary API and may be removed in a future release - sun.misc.VM.saveAndRemoveProperties(properties); - ^ -14 warnings - -> Task :jpf-core:compilePeersJava -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:32: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release -import sun.misc.Unsafe; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:93: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release - private static Unsafe unsafe; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:99: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release - Field singletonField = Unsafe.class.getDeclaredField("theUnsafe"); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:101: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release - unsafe = (Unsafe)singletonField.get(null); - ^ -4 warnings > Task :jpf-core:compileTestJava -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:34: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - Class callerCls = sun.reflect.Reflection.getCallerClass(0); // that would be getCallerClass() - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:38: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - callerCls = sun.reflect.Reflection.getCallerClass(1); // foo() - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:42: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - callerCls = sun.reflect.Reflection.getCallerClass(2); // bar() - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:46: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - callerCls = sun.reflect.Reflection.getCallerClass(3); // callIt() - ^ -Note: /Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java uses or overrides a deprecated API. +Note: Some input files use or override a deprecated API. Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. -4 warnings -Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. -Use '--warning-mode all' to show the individual deprecation warnings. -See https://docs.gradle.org/6.9.2/userguide/command_line_interface.html#sec:command_line_warnings +Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. + +You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. + +For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. -BUILD SUCCESSFUL in 6s -15 actionable tasks: 15 executed +BUILD SUCCESSFUL in 4s +16 actionable tasks: 16 executed ``` @@ -205,19 +119,32 @@ jpf-core jpf-symbc > Task :jpf-symbc:compileJava +Note: Some input files use or override a deprecated API. +Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. > Task :jpf-symbc:compileExamplesJava +Note: Some input files use or override a deprecated API. +Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. -Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. -Use '--warning-mode all' to show the individual deprecation warnings. -See https://docs.gradle.org/6.9.2/userguide/command_line_interface.html#sec:command_line_warnings +> Task :jpf-symbc:compilePeersJava +Note: /Users/aosenxiong/spf/jpf-symbc/jpf-symbc/src/peers/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java uses or overrides a deprecated API. +Note: Recompile with -Xlint:deprecation for details. + +> Task :jpf-symbc:compileTestJava +Note: Some input files use or override a deprecated API. +Note: Recompile with -Xlint:deprecation for details. + +Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. + +You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. + +For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. -BUILD SUCCESSFUL in 7s -12 actionable tasks: 12 executed +BUILD SUCCESSFUL in 2s ``` @@ -429,109 +356,23 @@ jpf-core jpf-symbc > Task :jpf-core:compileJava -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:21: warning: sun.misc.SharedSecrets is internal proprietary API and may be removed in a future release -import sun.misc.SharedSecrets; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:22: warning: sun.misc.JavaLangAccess is internal proprietary API and may be removed in a future release -import sun.misc.JavaLangAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:85: warning: sun.misc.JavaLangAccess is internal proprietary API and may be removed in a future release - static final JavaLangAccess JLA = SharedSecrets.getJavaLangAccess(); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:85: warning: sun.misc.SharedSecrets is internal proprietary API and may be removed in a future release - static final JavaLangAccess JLA = SharedSecrets.getJavaLangAccess(); - ^ -Note: /Users/yannic/Desktop/SPF/jpf-core/src/main/gov/nasa/jpf/vm/choice/PermutationCG.java uses or overrides a deprecated API. -Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. -4 warnings - -> Task :jpf-core:compileClassesJava -/Users/yannic/Desktop/SPF/jpf-core/src/classes/java/lang/ClassLoader.java:29: warning: sun.misc.CompoundEnumeration is internal proprietary API and may be removed in a future release -import sun.misc.CompoundEnumeration; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/java/lang/ClassLoader.java:114: warning: sun.misc.CompoundEnumeration is internal proprietary API and may be removed in a future release - return new CompoundEnumeration(resEnum); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/JavaNetAccess.java:32: warning: sun.misc.URLClassPath is internal proprietary API and may be removed in a future release - URLClassPath getURLClassPath (URLClassLoader ucl); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:52: warning: sun.misc.JavaUtilJarAccess is internal proprietary API and may be removed in a future release - private static JavaUtilJarAccess javaUtilJarAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:60: warning: sun.misc.JavaOISAccess is internal proprietary API and may be removed in a future release - private static JavaOISAccess javaOISAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:61: warning: sun.misc.JavaObjectInputStreamAccess is internal proprietary API and may be removed in a future release - private static JavaObjectInputStreamAccess javaObjectInputStreamAccess; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:82: warning: sun.misc.JavaUtilJarAccess is internal proprietary API and may be removed in a future release - public static JavaUtilJarAccess javaUtilJarAccess() { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:88: warning: sun.misc.JavaUtilJarAccess is internal proprietary API and may be removed in a future release - public static void setJavaUtilJarAccess(JavaUtilJarAccess access) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:142: warning: sun.misc.JavaObjectInputStreamAccess is internal proprietary API and may be removed in a future release - public static JavaObjectInputStreamAccess getJavaObjectInputStreamAccess() { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:151: warning: sun.misc.JavaObjectInputStreamAccess is internal proprietary API and may be removed in a future release - public static void setJavaObjectInputStreamAccess(JavaObjectInputStreamAccess access) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:162: warning: sun.misc.JavaOISAccess is internal proprietary API and may be removed in a future release - public static void setJavaOISAccess(JavaOISAccess access) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:166: warning: sun.misc.JavaOISAccess is internal proprietary API and may be removed in a future release - public static JavaOISAccess getJavaOISAccess() { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/sun/misc/SharedSecrets.java:175: warning: sun.misc.JavaObjectInputStreamReadString is internal proprietary API and may be removed in a future release - public void setJavaObjectInputStreamReadString(sun.misc.JavaObjectInputStreamReadString ignored) { - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/classes/java/lang/System.java:64: warning: sun.misc.VM is internal proprietary API and may be removed in a future release - sun.misc.VM.saveAndRemoveProperties(properties); - ^ -14 warnings - -> Task :jpf-core:compilePeersJava -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:32: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release -import sun.misc.Unsafe; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:93: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release - private static Unsafe unsafe; - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:99: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release - Field singletonField = Unsafe.class.getDeclaredField("theUnsafe"); - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:101: warning: sun.misc.Unsafe is internal proprietary API and may be removed in a future release - unsafe = (Unsafe)singletonField.get(null); - ^ -4 warnings > Task :jpf-core:compileTestJava -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:34: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - Class callerCls = sun.reflect.Reflection.getCallerClass(0); // that would be getCallerClass() - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:38: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - callerCls = sun.reflect.Reflection.getCallerClass(1); // foo() - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:42: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - callerCls = sun.reflect.Reflection.getCallerClass(2); // bar() - ^ -/Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:46: warning: sun.reflect.Reflection is internal proprietary API and may be removed in a future release - callerCls = sun.reflect.Reflection.getCallerClass(3); // callIt() - ^ -Note: /Users/yannic/Desktop/SPF/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java uses or overrides a deprecated API. +Note: Some input files use or override a deprecated API. Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. -4 warnings -Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. -Use '--warning-mode all' to show the individual deprecation warnings. -See https://docs.gradle.org/6.9.2/userguide/command_line_interface.html#sec:command_line_warnings +Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. + +You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. + +For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. -BUILD SUCCESSFUL in 6s -15 actionable tasks: 15 executed +BUILD SUCCESSFUL in 4s +16 actionable tasks: 16 executed ``` @@ -549,19 +390,32 @@ jpf-core jpf-symbc > Task :jpf-symbc:compileJava +Note: Some input files use or override a deprecated API. +Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. > Task :jpf-symbc:compileExamplesJava +Note: Some input files use or override a deprecated API. +Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. -Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. -Use '--warning-mode all' to show the individual deprecation warnings. -See https://docs.gradle.org/6.9.2/userguide/command_line_interface.html#sec:command_line_warnings +> Task :jpf-symbc:compilePeersJava +Note: /Users/aosenxiong/spf/jpf-symbc/jpf-symbc/src/peers/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java uses or overrides a deprecated API. +Note: Recompile with -Xlint:deprecation for details. + +> Task :jpf-symbc:compileTestJava +Note: Some input files use or override a deprecated API. +Note: Recompile with -Xlint:deprecation for details. + +Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. + +You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. + +For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. -BUILD SUCCESSFUL in 7s -12 actionable tasks: 12 executed +BUILD SUCCESSFUL in 2s ``` @@ -571,33 +425,58 @@ BUILD SUCCESSFUL in 7s > cd SPF > ./gradlew :jpf-core:buildJars jpf-core - jpf-symbc - - Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. - Use '--warning-mode all' to show the individual deprecation warnings. - See https://docs.gradle.org/6.9/userguide/command_line_interface.html#sec:command_line_warnings - - BUILD SUCCESSFUL in 2s - 15 actionable tasks: 2 executed, 13 up-to-date + jpf-symbc + + > Task :jpf-core:compileJava + Note: Some input files use unchecked or unsafe operations. + Note: Recompile with -Xlint:unchecked for details. + + > Task :jpf-core:compileTestJava + Note: Some input files use or override a deprecated API. + Note: Recompile with -Xlint:deprecation for details. + Note: Some input files use unchecked or unsafe operations. + Note: Recompile with -Xlint:unchecked for details. + + Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. + + You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. + + For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. + + BUILD SUCCESSFUL in 4s + 16 actionable tasks: 16 executed > ./gradlew :jpf-symbc:buildJars - jpf-core - jpf-symbc - - > Task :jpf-symbc:compileJava - Note: Some input files use unchecked or unsafe operations. - Note: Recompile with -Xlint:unchecked for details. - - > Task :jpf-symbc:compileExamplesJava - Note: Some input files use unchecked or unsafe operations. - Note: Recompile with -Xlint:unchecked for details. - - Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. - Use '--warning-mode all' to show the individual deprecation warnings. - See https://docs.gradle.org/6.9/userguide/command_line_interface.html#sec:command_line_warnings - - BUILD SUCCESSFUL in 20s - 12 actionable tasks: 12 executed + jpf-core + jpf-symbc + + > Task :jpf-symbc:compileJava + Note: Some input files use or override a deprecated API. + Note: Recompile with -Xlint:deprecation for details. + Note: Some input files use unchecked or unsafe operations. + Note: Recompile with -Xlint:unchecked for details. + + > Task :jpf-symbc:compileExamplesJava + Note: Some input files use or override a deprecated API. + Note: Recompile with -Xlint:deprecation for details. + Note: Some input files use unchecked or unsafe operations. + Note: Recompile with -Xlint:unchecked for details. + + > Task :jpf-symbc:compilePeersJava + Note: /Users/aosenxiong/spf/jpf-symbc/jpf-symbc/src/peers/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java uses or overrides a deprecated API. + Note: Recompile with -Xlint:deprecation for details. + + > Task :jpf-symbc:compileTestJava + Note: Some input files use or override a deprecated API. + Note: Recompile with -Xlint:deprecation for details. + + Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. + + You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. + + For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. + + BUILD SUCCESSFUL in 2s ``` --> @@ -684,9 +563,9 @@ gov.nasa.jpf.symbc.TestSwitch > mainTest PASSED Test Execution: SUCCESS Summary: 24 tests, 24 passed, 0 failed, 0 skipped -Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0. -Use '--warning-mode all' to show the individual deprecation warnings. -See https://docs.gradle.org/6.9.2/userguide/command_line_interface.html#sec:command_line_warnings +Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0. +You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins. +For more on this, please refer to https://docs.gradle.org/8.4/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation. BUILD SUCCESSFUL in 21s 13 actionable tasks: 6 executed, 7 up-to-date diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 549d8442..e411586a 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-6.9-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/jpf-core b/jpf-core index 45a4450c..579284ff 160000 --- a/jpf-core +++ b/jpf-core @@ -1 +1 @@ -Subproject commit 45a4450cd0bd1193df5419f7c9d9b89807d00db6 +Subproject commit 579284ff82cac0b2bc1fe5441af47aa32fcd7bf7 diff --git a/jpf-symbc/build.gradle b/jpf-symbc/build.gradle index b07cc738..dfc4ada3 100644 --- a/jpf-symbc/build.gradle +++ b/jpf-symbc/build.gradle @@ -7,8 +7,10 @@ def getCurrentVersion() { version = currentVersion -sourceCompatibility = 1.8 -targetCompatibility = 1.8 +java { + sourceCompatibility = JavaVersion.VERSION_11 + targetCompatibility = JavaVersion.VERSION_11 +} repositories { mavenCentral() @@ -59,6 +61,11 @@ dependencies { } +compileTestJava.dependsOn copyResources +compileExamplesJava.dependsOn copyResources +compilePeersJava.dependsOn copyResources +compileClassesJava.dependsOn copyResources + task compile { group = "SPF Build" description = "Compiles all JPF symbc sources." @@ -71,34 +78,34 @@ task compile { } task createJpfClassesJar(type: Jar) { - archiveName = "jpf-symbc-classes.jar" - destinationDir = file("${buildDir}") + archiveFileName = "jpf-symbc-classes.jar" + destinationDirectory = file("${buildDir}") group = "SPF Jars" - description = "Creates the ${archiveName} file." + description = "Creates the ${archiveFileName} file." dependsOn compile dependsOn copyResources - from sourceSets.main.java.outputDir - from sourceSets.annotations.java.outputDir - from sourceSets.classes.java.outputDir + from sourceSets.main.output.classesDirs + from sourceSets.annotations.output.classesDirs + from sourceSets.classes.output.classesDirs } task createJpfJar(type: Jar) { - archiveName = "jpf-symbc.jar" - destinationDir = file("${buildDir}") + archiveFileName = "jpf-symbc.jar" + destinationDirectory = file("${buildDir}") group = "SPF Jars" - description = "Creates the ${archiveName} file." + description = "Creates the ${archiveFileName} file." dependsOn compile dependsOn copyResources - from sourceSets.main.java.outputDir - from sourceSets.peers.java.outputDir - from sourceSets.annotations.java.outputDir - from sourceSets.classes.java.outputDir + from sourceSets.main.output.classesDirs + from sourceSets.peers.output.classesDirs + from sourceSets.annotations.output.classesDirs + from sourceSets.classes.output.classesDirs manifest { attributes "Implementation-Title": "Symbolic Pathfinder system" @@ -107,16 +114,16 @@ task createJpfJar(type: Jar) { } task createAnnotationsJar(type: Jar) { - archiveName = "jpf-symbc-annotations.jar" - destinationDir = file("${buildDir}") + archiveFileName = "jpf-symbc-annotations.jar" + destinationDirectory = file("${buildDir}") group = "SPF Jars" - description = "Creates the ${archiveName} file." + description = "Creates the ${archiveFileName} file." dependsOn compile dependsOn copyResources - from sourceSets.annotations.java.outputDir + from sourceSets.annotations.output.classesDirs } task buildJars { diff --git a/jpf-symbc/gradle/build-resources.gradle b/jpf-symbc/gradle/build-resources.gradle index 760fc545..5204e16a 100644 --- a/jpf-symbc/gradle/build-resources.gradle +++ b/jpf-symbc/gradle/build-resources.gradle @@ -43,8 +43,8 @@ task copyResources(type: Copy) { dependsOn generateVersion from new File(projectDir, "build.properties") - into sourceSets.main.java.outputDir.path + "/gov/nasa/jpf" + into sourceSets.main.output.classesDirs.getSingleFile().path + "/gov/nasa/jpf" from new File(projectDir, ".version") - into sourceSets.main.java.outputDir.path + "/gov/nasa/jpf" -} \ No newline at end of file + into sourceSets.main.output.classesDirs.getSingleFile().path + "/gov/nasa/jpf" +} diff --git a/jpf-symbc/gradle/distribution.gradle b/jpf-symbc/gradle/distribution.gradle index 1006249e..72eed30a 100644 --- a/jpf-symbc/gradle/distribution.gradle +++ b/jpf-symbc/gradle/distribution.gradle @@ -2,12 +2,12 @@ task srcDist(type: Zip) { group = "SPF Distribution" description = "Builds the source distribution." - baseName = project.name - version = project.version - classifier = "src" - extension = "zip" + archiveBaseName = project.name + archiveVersion = project.version + archiveClassifier = "src" + archiveExtension = "zip" - destinationDir = buildDir + destinationDirectory = buildDir includeEmptyDirs = false from projectDir @@ -28,11 +28,11 @@ task dist(type: Zip) { group = "SPF Distribution" description = "Builds binary distribution." - baseName = project.name - version = project.version - extension = "zip" + archiveBaseName = project.name + archiveVersion = project.version + archiveExtension = "zip" - destinationDir = buildDir + destinationDirectory = buildDir includeEmptyDirs = false from projectDir diff --git a/jpf-symbc/gradle/source-sets.gradle b/jpf-symbc/gradle/source-sets.gradle index 75f2b372..5145a121 100644 --- a/jpf-symbc/gradle/source-sets.gradle +++ b/jpf-symbc/gradle/source-sets.gradle @@ -1,31 +1,31 @@ sourceSets { annotations { java.srcDirs = ["src/annotations"] - java.outputDir = file("${buildDir}/annotations") + java.destinationDirectory.set(file("${buildDir}/annotations")) } main { java.srcDirs = ["src/main"] - java.outputDir = file("${buildDir}/main") + java.destinationDirectory.set(file("${buildDir}/main")) compileClasspath += sourceSets.annotations.output } classes { java.srcDirs = ["src/classes"] - java.outputDir = file("${buildDir}/classes") + java.destinationDirectory.set(file("${buildDir}/classes")) compileClasspath += sourceSets.main.output + sourceSets.annotations.output } peers { java.srcDirs = ["src/peers"] - java.outputDir = file("${buildDir}/peers") + java.destinationDirectory.set(file("${buildDir}/peers")) compileClasspath += sourceSets.main.output + sourceSets.annotations.output } examples { java.srcDirs = ["src/examples"] - java.outputDir = file("${buildDir}/examples") + java.destinationDirectory.set(file("${buildDir}/examples")) compileClasspath += sourceSets.main.output + sourceSets.annotations.output + sourceSets.classes.output } test { java.srcDirs = ["src/tests"] - java.outputDir = file("${buildDir}/tests") + java.destinationDirectory.set(file("${buildDir}/tests")) compileClasspath += sourceSets.annotations.output + sourceSets.classes.output + sourceSets.peers.output runtimeClasspath += compileClasspath } diff --git a/jpf-symbc/gradle/wrapper/gradle-wrapper.properties b/jpf-symbc/gradle/wrapper/gradle-wrapper.properties index 7665b0fa..fce403e4 100644 --- a/jpf-symbc/gradle/wrapper/gradle-wrapper.properties +++ b/jpf-symbc/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-6.9-all.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-all.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/jpf-symbc/src/classes/java/awt/image/BufferedImage.java b/jpf-symbc/src/classes/java/awt/image/BufferedImage.java deleted file mode 100644 index 1e6b7142..00000000 --- a/jpf-symbc/src/classes/java/awt/image/BufferedImage.java +++ /dev/null @@ -1,185 +0,0 @@ -/* - * Copyright (c) 1997, 2013, Oracle and/or its affiliates. All rights reserved. - * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. - * - * This code is free software; you can redistribute it and/or modify it - * under the terms of the GNU General Public License version 2 only, as - * published by the Free Software Foundation. Oracle designates this - * particular file as subject to the "Classpath" exception as provided - * by Oracle in the LICENSE file that accompanied this code. - * - * This code is distributed in the hope that it will be useful, but WITHOUT - * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or - * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License - * version 2 for more details (a copy is included in the LICENSE file that - * accompanied this code). - * - * You should have received a copy of the GNU General Public License version - * 2 along with this work; if not, write to the Free Software Foundation, - * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. - * - * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA - * or visit www.oracle.com if you need additional information or have any - * questions. - */ - -package java.awt.image; - -import gov.nasa.jpf.symbc.Debug; - -/** - * - * Minimal model for BufferedImage that makes everything symbolic. - * - * @author Rody Kersten - */ - -public class BufferedImage // extends java.awt.Image -// implements WritableRenderedImage, Transparency -{ - // Simple model: just int width and height, plus 2-dimensional array of pixels. - int width; - int height; - int pixels[][]; - - // each symbolic image has a unique ID - int id; - static int nextID = 0; - - // has all these defines - public static final int TYPE_CUSTOM = 0; - public static final int TYPE_INT_RGB = 1; - public static final int TYPE_INT_ARGB = 2; - public static final int TYPE_INT_ARGB_PRE = 3; - public static final int TYPE_INT_BGR = 4; - public static final int TYPE_3BYTE_BGR = 5; - public static final int TYPE_4BYTE_ABGR = 6; - public static final int TYPE_4BYTE_ABGR_PRE = 7; - public static final int TYPE_USHORT_565_RGB = 8; - public static final int TYPE_USHORT_555_RGB = 9; - public static final int TYPE_BYTE_GRAY = 10; - public static final int TYPE_USHORT_GRAY = 11; - public static final int TYPE_BYTE_BINARY = 12; - public static final int TYPE_BYTE_INDEXED = 13; - - public BufferedImage(int width, int height, int imageType) { - this.width = width; - this.height = height; - this.pixels = new int[width][height]; - this.id = nextID++; - -// // symbolic pixels -// for (int x = 0; x < width; x++) { -// for (int y = 0; y < height; y++) { -// pixels[x][y] = Debug.makeSymbolicInteger("image" + id + "pixel" + x + ":" + y); -// } -// } - } - - public BufferedImage(int width, int height, int imageType, IndexColorModel cm) { - this(width, height, imageType); - } - - public int getType() { - return TYPE_INT_ARGB; - } - - public int getRGB(int x, int y) { - return pixels[x][y]; - } - - public int[] getRGB(int startX, int startY, int w, int h, int[] rgbArray, int offset, int scansize) { - if (rgbArray == null) { - rgbArray = new int[w * h]; - offset = 0; - } - - int i = 0; - for (int x = startX; x < startX + w; x++) { - for (int y = startY; y < startY + h; y++) { - rgbArray[i++] = pixels[x][y]; - } - } - - return rgbArray; - } - - public synchronized void setRGB(int x, int y, int rgb) { - pixels[x][y] = rgb; - } - - // public void setRGB(int startX, int startY, int w, int h, - // int[] rgbArray, int offset, int scansize) { - // //TODO - // } - - public int getWidth() { - return width; - } - - public int getHeight() { - return height; - } - - public int getWidth(ImageObserver observer) { - return width; - } - - public int getHeight(ImageObserver observer) { - return height; - } - - // public BufferedImage getSubimage (int x, int y, int w, int h) { - // //TODO - // } - - public String toString() { - return "Symbolic BufferedImage"; - } - - public int getMinX() { - return 0; - } - - public int getMinY() { - return 0; - } - - public int getNumXTiles() { - return 1; - } - - public int getNumYTiles() { - return 1; - } - - public int getMinTileX() { - return 0; - } - - public int getMinTileY() { - return 0; - } - - public int getTileWidth() { - return width; - } - - public int getTileHeight() { - return height; - } - - public BufferedImage getCopy() { - BufferedImage copy = new BufferedImage(width, height, 0); - for (int x = 0; x < width; x++) { - for (int y = 0; y < height; y++) { - copy.setRGB(x, y, pixels[x][y]); - } - } - return copy; - } - - public ColorModel getColorModel() { - return null; - } -} diff --git a/jpf-symbc/src/classes/java/awt/image/Kernel.java b/jpf-symbc/src/classes/java/awt/image/Kernel.java deleted file mode 100644 index 0dad716a..00000000 --- a/jpf-symbc/src/classes/java/awt/image/Kernel.java +++ /dev/null @@ -1,153 +0,0 @@ -/* - * Copyright (c) 1997, 2011, Oracle and/or its affiliates. All rights reserved. - * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. - * - * This code is free software; you can redistribute it and/or modify it - * under the terms of the GNU General Public License version 2 only, as - * published by the Free Software Foundation. Oracle designates this - * particular file as subject to the "Classpath" exception as provided - * by Oracle in the LICENSE file that accompanied this code. - * - * This code is distributed in the hope that it will be useful, but WITHOUT - * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or - * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License - * version 2 for more details (a copy is included in the LICENSE file that - * accompanied this code). - * - * You should have received a copy of the GNU General Public License version - * 2 along with this work; if not, write to the Free Software Foundation, - * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. - * - * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA - * or visit www.oracle.com if you need additional information or have any - * questions. - */ - -package java.awt.image; - - -/** - * The Kernel class defines a matrix that describes how a - * specified pixel and its surrounding pixels affect the value - * computed for the pixel's position in the output image of a filtering - * operation. The X origin and Y origin indicate the kernel matrix element - * that corresponds to the pixel position for which an output value is - * being computed. - * - * @see ConvolveOp - */ -public class Kernel implements Cloneable { - private int width; - private int height; - private int xOrigin; - private int yOrigin; - private float data[]; - - private static native void initIDs(); - static { -// ColorModel.loadLibraries(); -// initIDs(); - } - - /** - * Constructs a Kernel object from an array of floats. - * The first width*height elements of - * the data array are copied. - * If the length of the data array is less - * than width*height, an IllegalArgumentException is thrown. - * The X origin is (width-1)/2 and the Y origin is (height-1)/2. - * @param width width of the kernel - * @param height height of the kernel - * @param data kernel data in row major order - * @throws IllegalArgumentException if the length of data - * is less than the product of width and - * height - */ - public Kernel(int width, int height, float data[]) { - this.width = width; - this.height = height; - this.xOrigin = (width-1)>>1; - this.yOrigin = (height-1)>>1; - int len = width*height; - if (data.length < len) { - throw new IllegalArgumentException("Data array too small "+ - "(is "+data.length+ - " and should be "+len); - } - this.data = new float[len]; - System.arraycopy(data, 0, this.data, 0, len); - - } - - /** - * Returns the X origin of this Kernel. - * @return the X origin. - */ - final public int getXOrigin(){ - return xOrigin; - } - - /** - * Returns the Y origin of this Kernel. - * @return the Y origin. - */ - final public int getYOrigin() { - return yOrigin; - } - - /** - * Returns the width of this Kernel. - * @return the width of this Kernel. - */ - final public int getWidth() { - return width; - } - - /** - * Returns the height of this Kernel. - * @return the height of this Kernel. - */ - final public int getHeight() { - return height; - } - - /** - * Returns the kernel data in row major order. - * The data array is returned. If data - * is null, a new array is allocated. - * @param data if non-null, contains the returned kernel data - * @return the data array containing the kernel data - * in row major order or, if data is - * null, a newly allocated array containing - * the kernel data in row major order - * @throws IllegalArgumentException if data is less - * than the size of this Kernel - */ - final public float[] getKernelData(float[] data) { - if (data == null) { - data = new float[this.data.length]; - } - else if (data.length < this.data.length) { - throw new IllegalArgumentException("Data array too small "+ - "(should be "+this.data.length+ - " but is "+ - data.length+" )"); - } - System.arraycopy(this.data, 0, data, 0, this.data.length); - - return data; - } - - /** - * Clones this object. - * @return a clone of this object. - */ - public Object clone() { - try { - return super.clone(); - } catch (CloneNotSupportedException e) { - // this shouldn't happen, since we are Cloneable - throw new InternalError(e); - } - } -} diff --git a/jpf-symbc/src/classes/java/lang/Math.java b/jpf-symbc/src/classes/java/lang/Math.java deleted file mode 100644 index 59791096..00000000 --- a/jpf-symbc/src/classes/java/lang/Math.java +++ /dev/null @@ -1,165 +0,0 @@ -/* - * Copyright (C) 2014, United States Government, as represented by the - * Administrator of the National Aeronautics and Space Administration. - * All rights reserved. - * - * Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License, - * Version 2.0 (the "License"); you may not use this file except - * in compliance with the License. You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0. - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -// -//Copyright (C) 2006 United States Government as represented by the -//Administrator of the National Aeronautics and Space Administration -//(NASA). All Rights Reserved. -// -//This software is distributed under the NASA Open Source Agreement -//(NOSA), version 1.3. The NOSA has been approved by the Open Source -//Initiative. See the file NOSA-1.3-JPF at the top of the distribution -//directory tree for the complete NOSA document. -// -//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY -//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT -//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO -//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR -//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT -//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT -//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. -// - -package java.lang; - -public class Math { - public static final double PI = 3.141592653589793; - - public static double abs ( double a) { - return (a < 0.0) ? -a : a; - } - - public static float abs ( float a) { - return (a < 0.0) ? - a : a; - } - - public static int abs ( int a) { - return (a < 0) ? -a : a; // that's probably slightly faster - } - - public static long abs ( long a) { - return (a < 0) ? -a : a; - } - - // TODO: - public static double max ( double a, double b) { - return (a >= b) ? a : b; - } - - // TODO: need to model NaN et al. - public static float max ( float a, float b) { - return (a >= b) ? a : b; - } - - public static int max ( int a, int b) { - return (a >= b) ? a : b; - } - - public static long max ( long a, long b) { - return (a >= b) ? a : b; - } - - // TODO: - public static double min ( double a, double b) { - return (a >= b) ? a : b; - } - - // TODO: - public static float min ( float a, float b) { - return (a <= b) ? a : b; - } - - public static int min ( int a, int b) { - return (a <= b) ? a : b; - } - - public static long min ( long a, long b) { - return (a <= b) ? a : b; - } - - public static long round ( double d) { - if (d > 0) { - return (long) (d + 0.5d); - } else { - return (long) (d - 0.5d); - } - } - - public static int round ( float d) { - if (d > 0) { - return (int) (d + 0.5d); - } else { - return (int) (d - 0.5d); - } - } - public native static double sqrt ( double a) ; - - public native static double random (); - - - - public native static double exp ( double a) ; - - public native static double asin ( double a) ; - - public native static double acos ( double a) ; - - public native static double atan ( double a); - - public native static double atan2 ( double a, double b); - -// TODO: fix - public static double ceil ( double a) { - long result = (long)a; - if (result < a) result ++; - - return result; - } - -// TODO: fix - public static double floor ( double a) { - long result = (long)a; - if (result > a) result --; - - return result; - } - - public native static double log ( double a); - - // TODO: fix - // Warning: this is different IEEE standard - public static double rint ( double a) { - System.err.println("Warning: Math.rint not modeled according to IEEE standard"); - - if (a >= 0) - return (long) (a + 0.5); - else - return (long) (a - 0.5); - } - - public native static double tan ( double a); - - public native static double sin ( double a); - - public native static double cos ( double a); - - public native static double pow ( double a, double b); - - public static native double log10(double a); - -} diff --git a/jpf-symbc/src/classes/java/util/Scanner.java b/jpf-symbc/src/classes/java/util/Scanner.java deleted file mode 100644 index f6beb73d..00000000 --- a/jpf-symbc/src/classes/java/util/Scanner.java +++ /dev/null @@ -1,18 +0,0 @@ -package java.util; - -import java.io.InputStream; - -import gov.nasa.jpf.symbc.Debug; - -/** - * @author Kasper Luckow - */ -public class Scanner { - - public Scanner(InputStream in) { } - - private static int symid = 0; - public String nextLine() { - return Debug.makeSymbolicString("SCAN_SYM_" + symid++); - } -} diff --git a/settings.gradle b/settings.gradle index b1086c26..efb244fc 100644 --- a/settings.gradle +++ b/settings.gradle @@ -1,3 +1,7 @@ +plugins { + id 'com.gradle.enterprise' version '3.13.4' +} + rootProject.name = 'SPF' include ':jpf-core'