Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/main' into newFinalHeaps
Browse files Browse the repository at this point in the history
  • Loading branch information
mattulbrich committed Feb 23, 2025
2 parents e921c72 + dfc5b50 commit e137c77
Show file tree
Hide file tree
Showing 56 changed files with 1,499 additions and 1,659 deletions.
2 changes: 1 addition & 1 deletion .github/pull_request_template.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ remain since they will be invisible when showing the PR.

<!-- Please remove if this PR is not related to an issue. -->
<!-- Please add number if it is in answer to an issue. -->
This pull request addresses #.
This pull request resolves #.

## Intended Change

Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/code_quality.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ jobs:
distribution: 'corretto'
cache: 'gradle'
- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: Build with Gradle
run: ./gradlew -DENABLE_NULLNESS=true compileTest

Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/gradle-publish.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ jobs:
server-id: github # Value of the distributionManagement/repository/id field of the pom.xml

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: Assemble with Gradle
run: ./gradlew assemble

Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/javadoc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ jobs:
distribution: 'corretto'
cache: 'gradle'
- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: Build Documentation with Gradle
run: ./gradlew alldoc

Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/nightlydeploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ jobs:
distribution: 'temurin'

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: Build with Gradle
run: ./gradlew --parallel assemble

Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/opttest.yml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ jobs:
cache: 'gradle'

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: Test with Gradle
run: ./gradlew --continue ${{ matrix.tests }}

Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/sonarqube.yml
Original file line number Diff line number Diff line change
Expand Up @@ -13,29 +13,29 @@ jobs:
name: Build and analyze
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: actions/checkout@v4
with:
fetch-depth: 0 # Shallow clones should be disabled for a better relevancy of analysis
- name: Set up JDK 21
uses: actions/setup-java@v3
uses: actions/setup-java@v4
with:
java-version: 21
distribution: 'zulu'
- name: Cache SonarCloud packages
uses: actions/cache@v3
uses: actions/cache@v4
with:
path: ~/.sonar/cache
key: ${{ runner.os }}-sonar
restore-keys: ${{ runner.os }}-sonar
- name: Cache Gradle packages
uses: actions/cache@v3
uses: actions/cache@v4
with:
path: ~/.gradle/caches
key: ${{ runner.os }}-gradle-${{ hashFiles('**/*.gradle') }}
restore-keys: ${{ runner.os }}-gradle

- name: Generate and submit dependency graph
uses: gradle/actions/dependency-submission@v3
uses: gradle/actions/dependency-submission@v4
with:
build-scan-publish: true
build-scan-terms-of-use-url: "https://gradle.com/terms-of-service"
Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ jobs:
cache: 'gradle'

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: Test with Gradle
run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test

Expand All @@ -53,7 +53,7 @@ jobs:
!**/jacocoTestReport.xml
- name: Upload coverage reports to Codecov
uses: codecov/codecov-action@v4
uses: codecov/codecov-action@v5

integration-tests:
env:
Expand Down Expand Up @@ -87,7 +87,7 @@ jobs:
shell: bash

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: "Running tests: ${{ matrix.test }}"
run: ./gradlew --continue ${{ matrix.test }}

Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/tests_winmac.yml
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ jobs:

- name: Setup Gradle
uses:
gradle/actions/setup-gradle@v4.1.0
gradle/actions/setup-gradle@v4
- name: Test with Gradle
run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test

Expand Down Expand Up @@ -76,7 +76,7 @@ jobs:
run: .github/dlsmt.sh

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v4.1.0
uses: gradle/actions/setup-gradle@v4
- name: "Running tests: ${{ matrix.test }}"
run: ./gradlew --continue ${{ matrix.test }}

Expand Down
17 changes: 9 additions & 8 deletions build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -24,9 +24,9 @@ plugins {
id "com.diffplug.spotless" version "6.25.0"

// EISOP Checker Framework
id "org.checkerframework" version "0.6.45"
id "org.checkerframework" version "0.6.48"

id("org.sonarqube") version "5.0.0.4638"
id("org.sonarqube") version "6.0.1.5171"
}

sonar {
Expand Down Expand Up @@ -87,25 +87,26 @@ subprojects {
dependencies {
implementation("org.slf4j:slf4j-api:2.0.16")
implementation("org.slf4j:slf4j-api:2.0.16")
testImplementation("ch.qos.logback:logback-classic:1.5.12")
testImplementation("ch.qos.logback:logback-classic:1.5.15")

//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'

compileOnly("org.jspecify:jspecify:1.0.0")
testCompileOnly("org.jspecify:jspecify:1.0.0")
def eisop_version = "3.42.0-eisop4"
def eisop_version = "3.42.0-eisop5"
compileOnly "io.github.eisop:checker-qual:$eisop_version"
compileOnly "io.github.eisop:checker-util:$eisop_version"
testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
checkerFramework "io.github.eisop:checker-qual:$eisop_version"
checkerFramework "io.github.eisop:checker:$eisop_version"

testImplementation("ch.qos.logback:logback-classic:1.5.12")
testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.3'
testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.3'
testImplementation("ch.qos.logback:logback-classic:1.5.15")
testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.4'
testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.4'
testImplementation project(':key.util')

testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.3'
testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.4'
}

tasks.withType(JavaCompile) {
Expand Down
7 changes: 7 additions & 0 deletions key.core.example/build.gradle
Original file line number Diff line number Diff line change
@@ -1,5 +1,12 @@
plugins {
id 'application'
}

description "Example project to use KeY's APIs"

mainClassName ="org.key_project.Main"

dependencies {
implementation project(":key.core")
implementation 'ch.qos.logback:logback-classic:1.5.15'
}
2 changes: 2 additions & 0 deletions key.core.example/src/main/java/org/key_project/Main.java
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ public class Main {
* @param args The start parameters.
*/
public static void main(String[] args) {
LOGGER.info("Starting KeY example application.");
File location = args.length == 1 ? new File(args[0]) : new File("example");
// Path to the source code folder/file or to a *.proof file
try {
Expand Down Expand Up @@ -90,6 +91,7 @@ private static void proveEnvironmemt(KeYEnvironment<?> env) {
final List<Contract> proofContracts = getContracts(env);

for (Contract contract : proofContracts) {
LOGGER.info("Found contract '" + contract.getDisplayName());
proveContract(env, contract);
}
} finally {
Expand Down
56 changes: 56 additions & 0 deletions key.core.example/src/main/resources/logback.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
<configuration>
<!-- disables logback configuration messages on start up, see #1725 -->
<!--<statusListener class="ch.qos.logback.core.status.NopStatusListener" />-->

<timestamp key="timestamp" datePattern="yyyyMMdd'T'HHmmss"/>

<appender name="FILE" class="ch.qos.logback.core.FileAppender">
<file>${user.home}/.key/logs/key_${timestamp}.log</file>
<append>false</append>
<encoder>
<charset>UTF-8</charset>
<!-- replace newlines by \n to allow line-based filtering (see LogView) -->
<pattern>%date|%level|%thread|%logger|%file:%line|%replace(%msg){'[\n\r]','\\n'}|%replace(%ex){'[\n\r]','\\n'}%nopex|%n</pattern>
<outputPatternAsHeader>true</outputPatternAsHeader>
</encoder>
</appender>

<appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
<encoder>
<pattern>[%date{HH:mm:ss.SSS}] %highlight(%-5level) %cyan(%logger{0}) - %msg%ex%n</pattern>
</encoder>
<!--
The threshold of this filter is also selected by the command line option "verbose <int>" where
SILENT = 0 (completely off)
NORMAL = 1
INFO = 2
DEBUG = 3
TRACE = 4
-->
<filter class="ch.qos.logback.classic.filter.ThresholdFilter">
<level>INFO</level>
</filter>
</appender>

<root level="trace">
<appender-ref ref="STDOUT"/>
<appender-ref ref="FILE"/>
</root>

<!--
A logger for development, also print to CONSOLE. This logger is not restricted by any command line options.
You should not use this code on the master branch.
-->
<appender name="STDERR" class="ch.qos.logback.core.ConsoleAppender">
<encoder>
<pattern>[%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n</pattern>
</encoder>
<filter class="ch.qos.logback.classic.filter.ThresholdFilter">
<level>TRACE</level>
</filter>
</appender>
<logger name="key.devel" level="DEBUG">
<appender-ref ref="STDERR"/>
</logger>

</configuration>
102 changes: 0 additions & 102 deletions key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java

This file was deleted.

Loading

0 comments on commit e137c77

Please sign in to comment.