Merge branch 'main' into weigl/codecov

.github/workflows/update_symbex_oracles.yml

@@ -0,0 +1,43 @@
+name: Update Symbex Oracles
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [ "main" ]
+
+permissions:
+  contents: write
+  issues: write
+  pull-requests: write
+  id-token: write
+
+jobs:
+  optional-tests:
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up JDK 11
+        uses: actions/setup-java@v3
+        with:
+          java-version: '11'
+          distribution: 'temurin'
+
+      - name: Build with Gradle
+        uses: gradle/[email protected]
+        with:
+          arguments: --continue -D UPDATE_TEST_ORACLE=true -D ORACLE_DIRECTORY=key.core.symbolic_execution/src/test/resources/testcase :key.core.symbolic_execution:test
+
+      - name: Make new branch
+        uses: EndBug/add-and-commit@v9
+        with:
+          add: 'key.core.symbolic_execution/src/test/resources/testcase'
+          author_name: Kiki
+          author_email: [email protected]
+          default_author: github_actions
+          message: 'Auto-Commit: update of the symbex oracle'
+          pull: '--rebase --autostash'
+          new_branch: update_oracle_${GITHUB_RUN_ID}_${GITHUB_RUN_NUMBER}
+
+      - name: Create Pull-Request
+        run: gh pr create --title "Update of the symbex oracle" --body "This is an automated Pull Request" -a "unp1" -B "main" -l "automatic" -H update_oracle_${GITHUB_RUN_ID}_${GITHUB_RUN_NUMBER}

build.gradle

@@ -88,14 +88,14 @@ subprojects {
 
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.7")
-        testImplementation("ch.qos.logback:logback-classic:1.4.6")
+        testImplementation("ch.qos.logback:logback-classic:1.4.7")
 
         //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0'
         //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
         implementation 'com.google.code.findbugs:jsr305:3.0.2'
 
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.9.3'
-        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.9.2'
+        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.9.3'
         testCompileOnly 'junit:junit:4.13.2'
         testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.9.3'
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.9.3'

key.core.symbolic_execution/build.gradle

@@ -5,4 +5,6 @@ dependencies {
 
 test {
     maxHeapSize = "4g"
+    systemProperty "UPDATE_TEST_ORACLE", System.getProperty("UPDATE_TEST_ORACLE")
+    systemProperty "ORACLE_DIRECTORY", System.getProperty("ORACLE_DIRECTORY")
 }

key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java

@@ -62,6 +62,9 @@
  * @author Martin Hentschel
  */
 public abstract class AbstractSymbolicExecutionTestCase {
+    private static final Logger LOGGER =
+        LoggerFactory.getLogger(AbstractSymbolicExecutionTestCase.class);
+
     /**
      * <p>
      * If this constant is {@code true} a temporary directory is created with new oracle files. The
@@ -76,7 +79,13 @@ public abstract class AbstractSymbolicExecutionTestCase {
      * they are outdated.
      * </p>
      */
-    public static final boolean CREATE_NEW_ORACLE_FILES_IN_TEMP_DIRECTORY = false;
+    public static final boolean CREATE_NEW_ORACLE_FILES_IN_TEMP_DIRECTORY =
+        Boolean.getBoolean("UPDATE_TEST_ORACLE");
+
+
+    static {
+        LOGGER.warn("UPDATE_TEST_ORACLE is set to {}", CREATE_NEW_ORACLE_FILES_IN_TEMP_DIRECTORY);
+    }
 
     /**
      * If the fast mode is enabled the step wise creation of models is disabled.
@@ -109,8 +118,6 @@ public abstract class AbstractSymbolicExecutionTestCase {
      * The directory which contains the KeY repository.
      */
     public static final File testCaseDirectory = FindResources.getTestCasesDirectory();
-    private static final Logger LOGGER =
-        LoggerFactory.getLogger(AbstractSymbolicExecutionTestCase.class);
 
     static {
         assertNotNull(testCaseDirectory, "Could not find test case directory");
@@ -131,6 +138,11 @@ public abstract class AbstractSymbolicExecutionTestCase {
         try {
             if (CREATE_NEW_ORACLE_FILES_IN_TEMP_DIRECTORY) {
                 directory = File.createTempFile("SYMBOLIC_EXECUTION", "ORACLE_DIRECTORY");
+                if (System.getProperty("ORACLE_DIRECTORY") != null
+                        && !System.getProperty("ORACLE_DIRECTORY").isBlank()) {
+                    directory = new File(System.getProperty("ORACLE_DIRECTORY"));
+                }
+                LOGGER.warn("Create oracle files in {}", directory);
                 directory.delete();
                 directory.mkdirs();
             }
@@ -1105,7 +1117,6 @@ protected static void stepReturn(DefaultUserInterfaceControl ui,
     }
 
 
-
     /**
      * Executes an "step return" global on all goals on the given
      * {@link SymbolicExecutionTreeBuilder}.

key.core.symbolic_execution/src/test/resources/logback.xml

@@ -1,5 +1,7 @@
 <configuration>
+    <!-- disables logback configuration messages on start up, see #1725 -->
     <statusListener class="ch.qos.logback.core.status.NopStatusListener" />
+
     <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
         <file>key.log</file>
         <append>false</append>

key.core/build.gradle

@@ -18,8 +18,8 @@ dependencies {
     javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0'
     antlr group: 'org.antlr', name: 'antlr', version: '3.5.3'   // use ANTLR version 3
 
-    antlr4 "org.antlr:antlr4:4.12.0"
-    api "org.antlr:antlr4-runtime:4.12.0"
+    antlr4 "org.antlr:antlr4:4.13.0"
+    api "org.antlr:antlr4-runtime:4.13.0"
     //implementation group: 'com.google.guava', name: 'guava', version: '28.1-jre'
 }