diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml deleted file mode 100644 index 719dbbaafb0..00000000000 --- a/.github/workflows/gradle-publish.yml +++ /dev/null @@ -1,35 +0,0 @@ -name: Publish - -on: - release: - types: [created] - -jobs: - build: - runs-on: ubuntu-latest - permissions: - contents: read - packages: write - - steps: - - uses: actions/checkout@v6 - - name: Set up JDK 21 - uses: actions/setup-java@v5 - with: - java-version: '21' - distribution: 'corretto' - cache: 'gradle' - server-id: github # Value of the distributionManagement/repository/id field of the pom.xml - - - name: Setup Gradle - uses: gradle/actions/setup-gradle@v5 - - name: Assemble with Gradle - run: ./gradlew assemble - - # The USERNAME and TOKEN need to correspond to the credentials environment variables used in - # the publishing section of your build.gradle - - name: Publish to GitHub Packages - run: ./gradlew publish - env: - USERNAME: ${{ github.actor }} - TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml deleted file mode 100644 index aaebddeb2b6..00000000000 --- a/.github/workflows/javadoc.yml +++ /dev/null @@ -1,38 +0,0 @@ -name: Javadoc - -on: - push: - branches: [ "main" ] - -jobs: - doc: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v6 - - run: ls -ld - - run: ls -lh 'gradle' - - - name: Set up JDK 21 - uses: actions/setup-java@v5 - with: - java-version: '21' - distribution: 'corretto' - cache: 'gradle' - - name: Setup Gradle - uses: gradle/actions/setup-gradle@v5 - - name: Build Documentation with Gradle - run: ./gradlew alldoc - - - name: Package - run: tar cvfj javadoc.tar.bz2 build/docs/javadoc - - - name: Upload Javadoc - uses: actions/upload-artifact@v5 - with: - name: javadoc - path: "javadoc.tar.bz2" - -# - name: Trigger workflow in key-javadoc -# run: gh workflow run -R keyproject/key-javadoc pages.yml -f RUN_ID=${{ github.run_id }} -# env: -# GH_TOKEN: ${{ github.token }} diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index e9e85e303b3..380fb1b369a 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -1,4 +1,4 @@ -name: Nightly Deployer of Weekly Builds +name: Weekly Builds of KeY on: workflow_dispatch: @@ -9,9 +9,12 @@ permissions: contents: write id-token: write +env: + JAVA_VERSION: 21 + jobs: - deploy: + build: runs-on: ubuntu-latest steps: # weigl: Should produce fancier release notes, but needs some configuration @@ -27,14 +30,52 @@ jobs: - name: Set up JDK 21 uses: actions/setup-java@v5 with: - java-version: 21 + java-version: ${{ env.JAVA_VERSION }} distribution: 'temurin' + cache: 'gradle' - name: Setup Gradle uses: gradle/actions/setup-gradle@v5 - name: Build with Gradle run: ./gradlew --parallel assemble + doc: + needs: [build] + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Set up JDK 21 + uses: actions/setup-java@v4 + with: + java-version: ${{ env.JAVA_VERSION }} + distribution: 'corretto' + cache: 'gradle' + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + + - name: Build Documentation with Gradle + run: ./gradlew alldoc + + - name: Package + run: tar cvf key-javadoc.tar.xz build/docs/javadoc + + deploy: + needs: [build, doc] + runs-on: ubuntu-latest + steps: + - name: Upload Javadoc + uses: actions/upload-artifact@v4 + with: + name: javadoc + path: "javadoc.tar.xz" + + - name: Upload ShadowJar + uses: actions/upload-artifact@v4 + with: + name: shadowjars + path: "*/build/libs/*-exe.jar" + - name: Delete previous nightly release continue-on-error: true env: @@ -50,3 +91,25 @@ jobs: gh release create --generate-notes --title "Nightly Release" \ --prerelease --notes-start-tag KEY-2.12.3 \ nightly key.ui/build/libs/key-*-exe.jar + + deploy-maven: + needs: [ build, doc ] + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Set up JDK 21 + uses: actions/setup-java@v4 + with: + java-version: ${{ env.JAVA_VERSION }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v4 + + - name: Upload to SNAPSHOT repository + run: ./gradlew publishToCentral + env: + BUILD_NUMBER: "SNAPSHOT" + ossrhUsername: ${{ secrets.MAVEN_CENTRAL_USER }} + ossrhPassword: ${{ secrets.MAVEN_CENTRAL_PASSWORD }} diff --git a/.github/workflows/sonarqube.yml b/.github/workflows/sonarqube.yml deleted file mode 100644 index cd898dc6045..00000000000 --- a/.github/workflows/sonarqube.yml +++ /dev/null @@ -1,49 +0,0 @@ -## Copied from SonarCloud - -name: SonarCloud -on: - push: - branches: - - main - pull_request: - types: [opened, synchronize, reopened] - -jobs: - build: - name: Build and analyze - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v6 - with: - fetch-depth: 0 # Shallow clones should be disabled for a better relevancy of analysis - - name: Set up JDK 21 - uses: actions/setup-java@v5 - with: - java-version: 21 - distribution: 'zulu' - - name: Cache SonarCloud packages - uses: actions/cache@v4 - with: - path: ~/.sonar/cache - key: ${{ runner.os }}-sonar - restore-keys: ${{ runner.os }}-sonar - - name: Cache Gradle packages - 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@v5 - with: - build-scan-publish: true - build-scan-terms-of-use-url: "https://gradle.com/terms-of-service" - build-scan-terms-of-use-agree: "yes" - - - name: Build and analyze - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # Needed to get PR information, if any - SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }} - GRADLE_OPTS: "-Xmx6g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8" - run: ./gradlew --parallel --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test classes testClasses :key.util:test jacocoTestReport sonar \ No newline at end of file diff --git a/build.gradle b/build.gradle index 87c74a426d9..a8e8694419c 100644 --- a/build.gradle +++ b/build.gradle @@ -1,5 +1,3 @@ -import groovy.transform.Memoized - plugins { //Support for IntelliJ IDEA //https://docs.gradle.org/current/userguide/idea_plugin.html @@ -9,9 +7,6 @@ plugins { //https://docs.gradle.org/current/userguide/eclipse_plugin.html id("eclipse") //support for Eclipse - // Gives `gradle dependencyUpdate` to show which dependency has a newer version - // id "com.github.ben-manes.versions" version "0.39.0" - // Code formatting id "com.diffplug.spotless" version "8.1.0" @@ -19,14 +14,9 @@ plugins { id "org.checkerframework" version "0.6.61" id("org.sonarqube") version "7.2.0.6526" -} -sonar { - properties { - property "sonar.projectKey", "KeYProject_key" - property "sonar.organization", "keyproject" - property "sonar.host.url", "https://sonarcloud.io" - } + // Plugin for publishing via the new Nexus API + id "io.github.gradle-nexus.publish-plugin" version "2.0.0" } @@ -57,8 +47,6 @@ subprojects { apply plugin: "eclipse" apply plugin: "com.diffplug.spotless" - apply plugin: "checkstyle" - apply plugin: "pmd" apply plugin: "org.checkerframework" group = rootProject.group @@ -71,9 +59,6 @@ subprojects { repositories { mavenCentral() - maven { - url = 'https://git.key-project.org/api/v4/projects/35/packages/maven' - } } dependencies { @@ -96,11 +81,10 @@ subprojects { testImplementation("ch.qos.logback:logback-classic:1.5.21") testImplementation(platform("org.junit:junit-bom:5.14.1")) - testImplementation ("org.junit.jupiter:junit-jupiter-api") - testImplementation ("org.junit.jupiter:junit-jupiter-api") - testImplementation ("org.junit.jupiter:junit-jupiter-params") - testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine") - testRuntimeOnly ("org.junit.platform:junit-platform-launcher") + testImplementation("org.junit.jupiter:junit-jupiter-api") + testImplementation("org.junit.jupiter:junit-jupiter-params") + testRuntimeOnly("org.junit.jupiter:junit-jupiter-engine") + testRuntimeOnly("org.junit.platform:junit-platform-launcher") testImplementation ("org.assertj:assertj-core:3.27.6") testImplementation project(':key.util') @@ -111,14 +95,14 @@ subprojects { testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.14.1' } - tasks.withType(JavaCompile) { + tasks.withType(JavaCompile).configureEach { // Setting UTF-8 as the java source encoding. options.encoding = "UTF-8" // Setting the release to Java 21 options.release = 21 } - tasks.withType(Javadoc) { + tasks.withType(Javadoc).configureEach { failOnError = false options.addBooleanOption 'Xdoclint:none', true //options.verbose() @@ -127,15 +111,13 @@ subprojects { } tasks.withType(Test).configureEach {//Configure all tests - def examplesDir = rootProject.layout.projectDirectory.dir("key.ui/examples").getAsFile() def runAllProofsReportDir = layout.buildDirectory.dir("report/runallproves/").get().getAsFile() - systemProperty "test-resources", "src/test/resources" systemProperty "testcases", "src/test/resources/testcase" systemProperty "TACLET_PROOFS", "tacletProofs" - systemProperty "EXAMPLES_DIR", "$examplesDir" - systemProperty "RUNALLPROOFS_DIR", "$runAllProofsReportDir" + systemProperty "EXAMPLES_DIR", file("$rootProject/key.ui/examples") + systemProperty "RUNALLPROOFS_DIR", layout.buildDirectory.dir("report/runallproves").get().toString() systemProperty "key.disregardSettings", "true" maxHeapSize = "4g" @@ -218,77 +200,6 @@ subprojects { classpath = sourceSets.test.runtimeClasspath } - // findbugs { findbugsTest.enabled = false; ignoreFailures = true } - pmd { - pmdTest.enabled = false - ignoreFailures = true - toolVersion = "7.10.0" - consoleOutput = false - rulesMinimumPriority = 5 - ruleSets = ["category/java/errorprone.xml", "category/java/bestpractices.xml"] - } - - tasks.register('pmdMainChanged', Pmd) { - // Specify all files that should be checked - def changedFiles = getChangedFiles() - source pmdMain.source.filter { f -> f.getAbsoluteFile().toString() in changedFiles } - classpath = checkstyleMain.classpath - reports { - html { - required = true - outputLocation = file("build/reports/pmd/main_diff.html") - } - xml { - required = true - outputLocation = file("build/reports/pmd/main_diff.xml") - } - } - } - - - checkstyle { - toolVersion = "10.26.0" - ignoreFailures = true - configFile = file("$rootDir/gradle/key_checks.xml") - showViolations = false // disable console output - } - - - tasks.register('checkstyleMainChanged', Checkstyle) { - // Specify all files that should be checked - def changedFiles = getChangedFiles() - source checkstyleMain.source.filter { f -> f.getAbsoluteFile().toString() in changedFiles } - classpath = checkstyleMain.classpath - - //println(source.getFiles()) - - // Define the output folder of the generated reports - reports { - html { - required = true - outputLocation = file("build/reports/checkstyle/main_diff.html") - } - xml { - required = true - outputLocation = file("build/reports/checkstyle/main_diff.xml") - } - } - } - - - // tasks.withType(FindBugs) { - // reports { - // xml.enabled = false - // html.enabled = true - // } - // } - tasks.withType(Pmd) { - reports { - xml.getRequired().set(true) - html.getRequired().set(true) - } - } - tasks.register('sourcesJar', Jar) { description = 'Create a jar file with the sources from this project' from sourceSets.main.allJava @@ -376,19 +287,6 @@ subprojects { } } -// checkerFramework { -// checkers = [ -// "org.checkerframework.checker.nullness.NullnessChecker", -// ] -// extraJavacArgs = [ -// "-AonlyDefs=^org\\.key_project\\.util", -// "-Xmaxerrs", "10000", -// "-Astubs=$projectDir/src/main/checkerframework", -// "-Werror", -// "-Aversion", -// ] -// } - afterEvaluate { // required so project.description is non-null as set by sub build.gradle publishing { publications { @@ -426,58 +324,29 @@ subprojects { } repositories { maven { - /** - * To be able to publish things on Maven Central, you need two things: - * - * (1) a JIRA account with permission on group-id `org.key-project` - * (2) a keyserver-published GPG (w/o sub-keys) - * - * Your `$HOME/.gradle/gradle.properties` should like this: - * ``` - * signing.keyId=YourKeyId - * signing.password=YourPublicKeyPassword - * ossrhUsername=your-jira-id - * ossrhPassword=your-jira-password - * ``` - * - * You can test signing with `gradle sign`, and publish with `gradle publish`. - * https://central.sonatype.org/publish/publish-guide/ - */ - if (project.version.endsWith("-SNAPSHOT")) { - name = "mavenSnapshot" - url = "https://s01.oss.sonatype.org/content/repositories/snapshots/" - credentials(PasswordCredentials) { - username = project.properties.getOrDefault("ossrhUsername", "") - password = project.properties.getOrDefault("ossrhPassword", "") - } - } else { - name = "mavenStaging" - url = "https://s01.oss.sonatype.org/service/local/staging/deploy/maven2/" - credentials(PasswordCredentials) { - username = project.properties.getOrDefault("ossrhUsername", "") - password = project.properties.getOrDefault("ossrhPassword", "") - } - } + name = "LOCAL" + url= uri("$rootDir/local") } - /* - maven { // deployment to git.key-project.org - name = "GitlabPackages" - url "https://git.key-project.org/api/v4/projects/35/packages/maven" - credentials(HttpHeaderCredentials) { - if (System.getenv("TOKEN") != null) { - name = 'Private-Token' - value = System.getenv("TOKEN") - } else { - name = 'Job-Token' - value = System.getenv("CI_JOB_TOKEN") + maven { // deployment to git.key-project.org/key-public/key + name = "KEYLAB" + url = uri("https://git.key-project.org/api/v4/projects/35/packages/maven") + credentials(HttpHeaderCredentials) { + // Gitlab supports three kinds of token. + if (System.getenv("TOKEN") != null) { + // Support for user token + name = 'Private-Token' + value = envOrPropertyValue("TOKEN") + } else { + // Support for Gitlab CI + name = 'Job-Token' + value = envOrPropertyValue("CI_JOB_TOKEN") + } + } + authentication { + header(HttpHeaderAuthentication) } } - authentication { - header(HttpHeaderAuthentication) - } - } - */ } } @@ -488,6 +357,38 @@ subprojects { } } + +nexusPublishing { + repositories { + central { + nexusUrl = uri("https://ossrh-staging-api.central.sonatype.com/service/local/") + snapshotRepositoryUrl = uri("https://central.sonatype.com/repository/maven-snapshots/") + + stagingProfileId.set("org.key-project") + + /** + * To be able to publish things on Maven Central, you need two things: + * + * (1) a JIRA account with permission on group-id `org.key-project` + * (2) a keyserver-published GPG (w/o sub-keys) + * + * Your `$HOME/.gradle/gradle.properties` should like this: + * ``` + * signing.keyId=YourKeyId + * signing.password=YourPublicKeyPassword + * ossrhUsername=your-jira-id + * ossrhPassword=your-jira-password + * ``` + * + * You can test signing with `gradle sign`, and publish with `gradle publish`. + * https://central.sonatype.org/publish/publish-guide/ + */ + username = envOrPropertyValue("ossrhUsername") + password = envOrPropertyValue("ossrhPassword") + } + } +} + tasks.register('start'){ description = "Use :key.ui:run instead" doFirst { @@ -506,8 +407,7 @@ tasks.register('alldoc', Javadoc){ destinationDir = layout.buildDirectory.dir("docs/javadoc").getOrNull().getAsFile() if (JavaVersion.current().isJava9Compatible()) { - //notworking on jenkins - //options.addBooleanOption('html5', true) + options.addBooleanOption('html5', true) } configure(options) { @@ -518,11 +418,9 @@ tasks.register('alldoc', Javadoc){ //stylesheetFile = new File( projectDir, 'src/javadoc/stylesheet.css' ) windowTitle = 'KeY API Documentation' docTitle = "KeY JavaDoc ($project.version) -- ${getDate()}" - bottom = "Copyright © 2003-2023 The KeY-Project." + bottom = "Copyright © 2003-2025 The KeY-Project." use = true - links += "https://docs.oracle.com/en/java/javase/17/docs/api/" - links += "http://www.antlr2.org/javadoc/" - links += "http://www.antlr3.org/api/Java/" + links += "https://docs.oracle.com/en/java/javase/21/docs/api/" links += "https://www.antlr.org/api/Java/" } } @@ -544,25 +442,10 @@ if (jacocoEnabled.toBoolean()) { } -@Memoized -def getChangedFiles() { - // Get the target and source branch - def anchor = "git merge-base HEAD origin/main".execute().getText() - - // Get list of all changed files including status - def allFiles = "git diff --name-status --diff-filter=dr $anchor".execute().getText().split("\n") - //println("Found ${allFiles.length} changed files") - - // Remove the status prefix - def files = new TreeSet() - for (file in allFiles) { - if (file.length() > 1) { - def a = file.substring(1).trim() - if (!a.isBlank()) { - files.add(("$rootDir/" + a).toString()) - } - } +def envOrPropertyValue(String key) { + if(key in System.getenv()) { + return System.getenv(key) + }else{ + return project.properties.getOrDefault(key, "$key-not-found") } - // Return the list of touched files - files -} +} \ No newline at end of file diff --git a/key.core.example/src/main/java/org/key_project/Main.java b/key.core.example/src/main/java/org/key_project/Main.java index ca565fbae3b..ef754b52d0e 100644 --- a/key.core.example/src/main/java/org/key_project/Main.java +++ b/key.core.example/src/main/java/org/key_project/Main.java @@ -57,7 +57,7 @@ public static void main(String[] args) { * * @param location the Path with the path to the source directory of the Java project * to be verified - * @return the {@KeYEnvironment} that provides the context for all following verification tasks + * @return the {@link KeYEnvironment} that provides the context for all following verification tasks * @throws ProblemLoaderException if the setup fails */ private static KeYEnvironment setupEnvironment(Path location) throws ProblemLoaderException { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/NameAbstractionTable.java b/key.core/src/main/java/de/uka/ilkd/key/java/NameAbstractionTable.java index ad8cfc36680..ff289fe64dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/NameAbstractionTable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/NameAbstractionTable.java @@ -43,7 +43,7 @@ public void add(SourceElement pe1, SourceElement pe2) { * * @param pe0 SourceElement * @param pe1 SourceElement - * @returns true if the pe1 and pe2 have been assigned to the same name + * @return true if the pe1 and pe2 have been assigned to the same name */ public boolean sameAbstractName(SourceElement pe0, SourceElement pe1) { if (declarations0 != null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java index 845fabb5d6f..8c88104bdaf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java @@ -453,7 +453,7 @@ public void setFactory(ITermProgramVariableCollectorFactory factory) { /** * sets the factory for origin term labels * - * @param originFactory the {@OriginTermLabelFactory} to use, if null is passed, origin labels + * @param originFactory the {@link OriginTermLabelFactory} to use, if null is passed, origin labels * should not be created */ public void setOriginFactory(OriginTermLabelFactory originFactory) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ConstructorDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ConstructorDeclaration.java index e06576c8307..9dab8048472 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ConstructorDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ConstructorDeclaration.java @@ -22,11 +22,11 @@ public class ConstructorDeclaration extends MethodDeclaration implements Constru /** * Constructor declaration. * - * @parm children an ExtList with the children. May include: a TypeReference (as a reference to - * the return type), a de.uka.ilkd.key.logic.ProgramElementName (as Name of the method), - * several ParameterDeclaration (as parameters of the declared method), a StatementBlock - * (as body of the declared method), several Modifier (taken as modifiers of the - * declaration), a Comment + * @param children an ExtList with the children. May include: a TypeReference (as a reference to + * the return type), a de.uka.ilkd.key.logic.ProgramElementName (as Name of the method), + * several ParameterDeclaration (as parameters of the declared method), a StatementBlock + * (as body of the declared method), several Modifier (taken as modifiers of the + * declaration), a Comment * @param parentIsInterfaceDeclaration a boolean set true iff parent is an InterfaceDeclaration */ public ConstructorDeclaration(ExtList children, boolean parentIsInterfaceDeclaration) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodBodyStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodBodyStatement.java index e6e973405b9..59993f490c7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodBodyStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodBodyStatement.java @@ -74,7 +74,7 @@ public void setBodySource(TypeReference bodySource) { /** * Get the exact Class the denoted method body is from. * - * @returns the TypeReference + * @return the TypeReference */ public TypeReference getBodySource() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java b/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java index 4f82244cc39..c26a3c9578d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java @@ -186,8 +186,8 @@ private void applyOnSubterm1(int varInd, ImmutableArray bo * application of this substitution. This is the case, if v occurrs free in * subTerm, but does not occurr in boundVars. * - * @returns true if subTerm bound by boundVars would change under - * application of this substitution + * @return true if subTerm bound by boundVars would change under + * application of this substitution */ protected boolean subTermChanges(ImmutableArray boundVars, JTerm subTerm) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java index a06965d49c2..718b06f6413 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java @@ -2256,7 +2256,7 @@ protected final StringBuilder translateFunc(Operator o, ArrayList * translate a bsum function. Alos add the created functionsymbol created depending on the term. * * @param bsumterm The term used as third argument of the bsum function. - * @pram sub The two terms used as first and second argument of the bsum operator. + * @param sub The two terms used as first and second argument of the bsum operator. * @return */ protected final StringBuilder translateBsumFunction(JTerm bsumterm, @@ -2294,7 +2294,7 @@ protected final StringBuilder translateBsumFunction(JTerm bsumterm, * term. * * @param bprodterm The term used as third argument of the bsum function. - * @pram sub The two terms used as first and second argument of the bsum operator. + * @param sub The two terms used as first and second argument of the bsum operator. * @return */ protected final StringBuilder translateBprodFunction(JTerm bprodterm, @@ -2330,7 +2330,7 @@ protected final StringBuilder translateBprodFunction(JTerm bprodterm, * * @param op the operator used for this function. * @param sorts the list of sort parameter of this function - * @result the function's result sort + * @return the function's result sort */ private void addFunction(Operator op, ArrayList sorts, Sort result, Services services) { if (!this.functionDecls.containsKey(op)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTSort.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTSort.java index 08c25ecf9f3..ff450e3f7b1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTSort.java @@ -8,7 +8,7 @@ /** * * - * @authors Aboubakr Achraf El Ghazi and Fikri Kabakcha + * @author Aboubakr Achraf El Ghazi, Fikri Kabakcha * */ public class SMTSort { diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java index b5a3406a89d..7eb9421937a 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java @@ -118,7 +118,6 @@ protected ProofAggregate parse(Path file) { * @param file problem file. * @param pro determines the profile that should be used. * @return ProofAggregate of the problem file. - * @profile determines the profile that should be used. */ protected ProofAggregate parse(Path file, Profile pro) { assertTrue(Files.exists(file)); diff --git a/key.ncore.calculus/build.gradle b/key.ncore.calculus/build.gradle index 0a75120fe68..05e0fe5994d 100644 --- a/key.ncore.calculus/build.gradle +++ b/key.ncore.calculus/build.gradle @@ -1,8 +1,3 @@ -plugins { } - -group = 'org.key-project' -version = '2.13.0' - repositories { mavenCentral() } @@ -10,11 +5,7 @@ repositories { dependencies { api project(':key.util') api project(':key.ncore') - implementation 'org.jspecify:jspecify:1.0.0' -} - -tasks.withType(Test) { - enableAssertions = true + implementation('org.jspecify:jspecify:1.0.0') } checkerFramework { diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java b/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java index 954abcc0537..232064588ad 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java @@ -100,7 +100,7 @@ public Semisequent succedent() { /// @return a string representation of the sequent @Override public String toString() { - return antecedent().toString() + "==>" + succedent().toString(); + return antecedent() + "==>" + succedent(); } /// Creates an iterator to traverse all [SequentFormula] objects in this sequent. @@ -154,12 +154,10 @@ public SequentFormula getFormulaByNr(int formulaNumber) { /// @param inAntecedent `true` to add the formula to the antecedent, `false` for the /// succedent /// @param first `true` to add the formula at the beginning, `false` to add it at the - /// end of the - /// selected semisequent + /// end of the selected semisequent /// @return a [SequentChangeInfo] containing the modified sequent and details of the change /// like which formulas have been added or removed (removal is possible as the - /// implementation guarantees - /// redundance freeness) + /// implementation guarantee redundancy freeness) public SequentChangeInfo addFormula(SequentFormula sequentFormula, boolean inAntecedent, boolean first) { final Semisequent seq = inAntecedent ? antecedent : succedent; @@ -273,7 +271,7 @@ private Semisequent createSemisequent(SemisequentChangeInfo semiCI) { /// Creates a new [Semisequent] composed of the list of formulas proved as argument /// - /// @param formulas the {@ImmutableList} of [SequentFormula]s used to create the + /// @param formulas the [ImmutableList] of [SequentFormula]s used to create the /// semisequent /// @return the [Semisequent] consisting of the provided formulas abstract protected Semisequent createSemisequent(final ImmutableList formulas); diff --git a/key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveMemberReference.java b/key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveMemberReference.java index c41ddca65ee..4421590de07 100644 --- a/key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveMemberReference.java +++ b/key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveMemberReference.java @@ -150,12 +150,9 @@ public ProblemReport analyze() { * return true iff the reference is a lhs of an assignment: Either an assignment operator or * ???. * - * @todo - * * @param reference * @return true iff the reference is a lhs of an assignment: Either an assignment operator or * ???. - * */ private static boolean isLHS(Reference reference) { NonTerminalProgramElement parent = reference.getASTParent(); @@ -229,7 +226,7 @@ private Type getFormalType() { *
  • MethodReference as parameter
    • * * - * @todo DAS IST JA WOHL NOCH NICHT + * todo DAS IST JA WOHL NOCH NICHT * * @return the resolved type */ diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java index 5553d9d6d7c..b6bfdaddfff 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java @@ -26,7 +26,7 @@ *

    * Provides the facility to open the documentation at press of F1. The opened page is determined * context-sensitive by the current focused component and parent components. Specify the URL via - * {@HelpInfo}. + * {@link HelpInfo}. * * @author Alexander Weigl * @version 1 (10.04.19) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index af3bf9cbfe4..72e683326c6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -52,8 +52,11 @@ protected SettingsPanel() { } /** - * @param info - * @return + * Factory method for the construction of informational displays using + * text areas. + * + * @param info information to be shown + * @return a new {@link JTextArea} showing the given information */ protected static JTextArea createInfoArea(String info) { JTextArea textArea = new JTextArea(info); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/GuiUtilities.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/GuiUtilities.java index baf3361a283..76a7fc9acdd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/GuiUtilities.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/GuiUtilities.java @@ -36,9 +36,11 @@ public static void copyHighlightToClipboard(SequentView view, PosInSequent pos) /** * Center a component on the screen. * + * Preconditions: comp.getSize() as on screen. + * * @param comp the component to be centered relative to the screen. It must already have its * final size set. - * @preconditions comp.getSize() as on screen. + * * @see #setCenter(Component, Component) */ public static void setCenter(Component comp) { diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index d83c99b9e90..8fb6d4e5f86 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -288,7 +288,7 @@ default List toList() { * predicate to apply to each element to determine if it * should be included * - * @returns the filtered list + * @return the filtered list */ default ImmutableList filter(Predicate predicate) { return Immutables.filter(this, predicate); diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index d8a428f3610..ac07e84a9b2 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/key.util/src/main/java/org/key_project/util/collection/Immutables.java @@ -182,7 +182,7 @@ private Immutables() { * predicate to apply to each element to determine if it * should be included * - * @returns the filtered list + * @return the filtered list */ public static ImmutableList filter(ImmutableList ts, Predicate predicate) { diff --git a/recoder/src/main/java/recoder/ProgramFactory.java b/recoder/src/main/java/recoder/ProgramFactory.java index 6956fa6c0eb..a54fe62f5b0 100644 --- a/recoder/src/main/java/recoder/ProgramFactory.java +++ b/recoder/src/main/java/recoder/ProgramFactory.java @@ -1717,7 +1717,7 @@ New createNew(ReferencePrefix accessPath, TypeReference constructorName, Volatile createVolatile(); /** - * Creates a new {@ling Annotation}. + * Creates a new {@link AnnotationUseSpecification}. * * @return a new instance of Annotation */ @@ -1873,7 +1873,7 @@ For createFor(ASTList inits, Expression guard, ASTListnull * - * @returns null + * @return null */ public StatementContainer getStatementContainer() { return null; } /** - * @throws UnsupportedOperationException * @see #getStatementContainer() */ public void setStatementContainer(@SuppressWarnings("unused") StatementContainer c) { diff --git a/recoder/src/main/java/recoder/kit/transformation/PrepareStatementList.java b/recoder/src/main/java/recoder/kit/transformation/PrepareStatementList.java index 5cd4eed2ea1..94b0ed2426b 100644 --- a/recoder/src/main/java/recoder/kit/transformation/PrepareStatementList.java +++ b/recoder/src/main/java/recoder/kit/transformation/PrepareStatementList.java @@ -19,7 +19,7 @@ /** * Syntactic transformation returning a mutable statement list that contains the given statement, - * and creating a new {@linkrecoder.java.StatementBlock} if necessary. It is necessary to create a + * and creating a new {@link recoder.java.StatementBlock} if necessary. It is necessary to create a * new block, if {@link recoder.kit.StatementKit#getStatementMutableList}returns null * . This is the case if the statement container allows only a single statement and the given * statement is not inside a {@link recoder.java.StatementBlock}. If the statement has no parent, it @@ -145,11 +145,6 @@ public Statement getStatement() { * Problem report indicating that a parent is not suited for a given child. */ public static class IllegalParentContext extends Conflict { - - /** - * serialization id - */ - private static final long serialVersionUID = -1995165154877949565L; private final NonTerminalProgramElement parent; public IllegalParentContext(NonTerminalProgramElement parent) {