Merge branch 'main' into weigl/abbrevmgr

.github/pull_request_template.md

@@ -0,0 +1,56 @@
+<!--
+Thanks for submitting this pull request for KeY.
+Since the project has a strict review policy, please make the
+reviewer's job easier by providing the necessary information
+in the text below. The comments may remain since they will be
+invisible when showing the PR.
+-->
+
+## Related Issue
+
+<!-- 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 #.
+
+## Intended Change
+
+<!-- Please give a brief description of what behaviour changes and 
+     why it should be changed. -->
+
+## Type of pull request
+
+<!--- What types of changes does your code introduce? Put an `x` in the box(es) that apply: -->
+
+- [ ] Bug fix (non-breaking change which fixes an issue)
+- [ ] Refactoring (behaviour should not change or only minimally change)
+- [ ] New feature (non-breaking change which adds functionality)
+- [ ] Breaking change (fix or feature that would cause existing functionality to change)
+- [ ] There are changes to the (Java) code
+- [ ] There are changes to the taclet rule base
+- [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
+- [ ] Other: 
+
+## Ensuring quality
+
+- [ ] I made sure that introduced/changed code is well documented (javadoc and inline comments).
+- [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
+- [ ] I added new test case(s) for new functionality.
+- [ ] I have tested the feature as follows: ...
+- [ ] I have checked that runtime performance has not deteriorated.
+
+## Additional information and contact(s)
+
+<!-- Add further information to help the reviewer understand the request.
+     Leave empty if you are sure the reviewer does not need more
+     
+     Who apart from yourself is involved in this pull request?
+     Use @mentions to refer to them here.
+     Use Co-Authored-By in your git commits if applicable. -->
+     
+<!-- DRAFT MODE: Please note that on the button to submit this pull
+     request you can select between submitting a merge-ready request
+     or one in draft mode (still evolving). 
+     Please use the draft mode unless you think that your proposal
+     should be brought onto master in the current form. -->
+
+The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

.github/release.yml

@@ -0,0 +1,28 @@
+# .github/release.yml
+
+# Documentation:
+# https://docs.github.com/en/repositories/releasing-projects-on-github/automatically-generated-release-notes
+
+changelog:
+  exclude:
+    labels:
+      - "Ignore in Changelog"
+    authors:
+      - octocat
+      - dependabot
+  categories:
+    - title: Breaking Changes 🗲
+      labels:
+        - "Breaking Change"
+    - title: Exciting New Features 🎉
+      labels:
+        - "Exciting New Feature"
+    - title: Enhancement
+      labels:
+        - "Enhancement"
+    - title: Bug Fixes
+      labels:
+        - "🐞 Bug"
+    - title: Other Changes
+      labels:
+        - "*"

codecov.yml

@@ -1,9 +1,15 @@
+coverage:
+  status:
+    project:
+      default:
+        informational: true
+
 github_checks:
   annotations: false
 
 ignore:
-  - "key.ui/"  
-  - "keyext.ui.testgen/"  
-  - "key.removegenerics/"  
-  - "key.core.symbolic_execution.example/"  
-  - "key.core.example/"    
+  - "key.ui/"
+  - "keyext.ui.testgen/" 
+  - "key.removegenerics/"
+  - "key.core.symbolic_execution.example/"
+  - "key.core.example/"

gradlew

@@ -83,10 +83,8 @@ done
 # This is normally unused
 # shellcheck disable=SC2034
 APP_BASE_NAME=${0##*/}
-APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
-
-# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
-DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+# Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036)
+APP_HOME=$( cd "${APP_HOME:-./}" > /dev/null && pwd -P ) || exit
 
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
@@ -133,10 +131,13 @@ location of your Java installation."
     fi
 else
     JAVACMD=java
-    which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
+    if ! command -v java >/dev/null 2>&1
+    then
+        die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
 
 Please set the JAVA_HOME variable in your environment to match the
 location of your Java installation."
+    fi
 fi
 
 # Increase the maximum file descriptors if we can.
@@ -197,6 +198,10 @@ if "$cygwin" || "$msys" ; then
     done
 fi
 
+
+# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+
 # Collect all arguments for the java command;
 #   * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
 #     shell script including quotes and variable substitutions, so put them in

key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java

@@ -26,19 +26,19 @@ public class TestGenerationSettings extends AbstractSettings {
     // endregion
 
     // region property names
-    private static final String PROP_APPLY_SYMBOLIC_EXECUTION =
-        "[TestGenSettings]applySymbolicExecution";
-    private static final String PROP_MAX_UWINDS = "[TestGenSettings]maxUnwinds";
-    private static final String PROP_OUTPUT_PATH = "[TestGenSettings]OutputPath";
-    private static final String PROP_REMOVE_DUPLICATES = "[TestGenSettings]RemoveDuplicates";
-    private static final String PROP_USE_RFL = "[TestGenSettings]UseRFL";
-    private static final String PROP_USE_JUNIT = "[TestGenSettings]UseJUnit";
-    private static final String PROP_CONCURRENT_PROCESSES = "[TestGenSettings]ConcurrentProcesses";
-    private static final String PROP_INVARIANT_FOR_ALL = "[TestGenSettings]InvariantForAll";
-    private static final String PROP_OPENJML_PATH = "[TestGenSettings]OpenJMLPath";
-    private static final String PROP_OBJENESIS_PATH = "[TestGenSettings]ObjenesisPath";
+    private static final String PROP_APPLY_SYMBOLIC_EXECUTION = "applySymbolicExecution";
+    private static final String PROP_MAX_UWINDS = "maxUnwinds";
+    private static final String PROP_OUTPUT_PATH = "OutputPath";
+    private static final String PROP_REMOVE_DUPLICATES = "RemoveDuplicates";
+    private static final String PROP_USE_RFL = "UseRFL";
+    private static final String PROP_USE_JUNIT = "UseJUnit";
+    private static final String PROP_CONCURRENT_PROCESSES = "ConcurrentProcesses";
+    private static final String PROP_INVARIANT_FOR_ALL = "InvariantForAll";
+    private static final String PROP_OPENJML_PATH = "OpenJMLPath";
+    private static final String PROP_OBJENESIS_PATH = "ObjenesisPath";
     private static final String PROP_INCLUDE_POST_CONDITION =
-        "[TestGenSettings]IncludePostCondition";
+        "IncludePostCondition";
+    private static final String CATEGORY = "TestGenSettings";
     // endregion
 
     // Option fields
@@ -56,14 +56,14 @@ public class TestGenerationSettings extends AbstractSettings {
 
 
     public TestGenerationSettings() {
-        applySymbolicExecution = TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX;
-        maxUnwinds = TestGenerationSettings.DEFAULT_MAXUNWINDS;
-        outputPath = TestGenerationSettings.DEFAULT_OUTPUTPATH;
-        removeDuplicates = TestGenerationSettings.DEFAULT_REMOVEDUPLICATES;
-        useRFL = TestGenerationSettings.DEFAULT_USERFL;
-        useJunit = TestGenerationSettings.DEFAULT_USEJUNIT;
-        concurrentProcesses = TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES;
-        invariantForAll = TestGenerationSettings.DEFAULT_INVARIANTFORALL;
+        applySymbolicExecution = DEFAULT_APPLYSYMBOLICEX;
+        maxUnwinds = DEFAULT_MAXUNWINDS;
+        outputPath = DEFAULT_OUTPUTPATH;
+        removeDuplicates = DEFAULT_REMOVEDUPLICATES;
+        useRFL = DEFAULT_USERFL;
+        useJunit = DEFAULT_USEJUNIT;
+        concurrentProcesses = DEFAULT_CONCURRENTPROCESSES;
+        invariantForAll = DEFAULT_INVARIANTFORALL;
         openjmlPath = DEFAULT_OPENJMLPATH;
         objenesisPath = DEFAULT_OBJENESISPATH;
         includePostCondition = DEFAULT_INCLUDEPOSTCONDITION;
@@ -128,39 +128,24 @@ public boolean includePostCondition() {
 
     @Override
     public void readSettings(Properties props) {
+        var prefix = "[" + CATEGORY + "]";
         setApplySymbolicExecution(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION,
-            TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX));
-        setMaxUnwinds(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_MAX_UWINDS,
-            TestGenerationSettings.DEFAULT_MAXUNWINDS));
-        setOutputPath(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_OUTPUT_PATH,
-            TestGenerationSettings.DEFAULT_OUTPUTPATH));
+            prefix + PROP_APPLY_SYMBOLIC_EXECUTION, DEFAULT_APPLYSYMBOLICEX));
+        setMaxUnwinds(SettingsConverter.read(props, prefix + PROP_MAX_UWINDS, DEFAULT_MAXUNWINDS));
+        setOutputPath(SettingsConverter.read(props, prefix + PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH));
         setRemoveDuplicates(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_REMOVE_DUPLICATES,
-            TestGenerationSettings.DEFAULT_REMOVEDUPLICATES));
-        setRFL(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_USE_RFL,
-            TestGenerationSettings.DEFAULT_USERFL));
-        setUseJunit(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_USE_JUNIT,
-            TestGenerationSettings.DEFAULT_USEJUNIT));
+            prefix + PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES));
+        setRFL(SettingsConverter.read(props, prefix + PROP_USE_RFL, DEFAULT_USERFL));
+        setUseJunit(SettingsConverter.read(props, prefix + PROP_USE_JUNIT, DEFAULT_USEJUNIT));
         setConcurrentProcesses(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_CONCURRENT_PROCESSES,
-            TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES));
+            prefix + PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES));
         setInvariantForAll(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_INVARIANT_FOR_ALL,
-            TestGenerationSettings.DEFAULT_INVARIANTFORALL));
-        setOpenjmlPath(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_OPENJML_PATH,
-            TestGenerationSettings.DEFAULT_OPENJMLPATH));
-        setObjenesisPath(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_OBJENESIS_PATH,
-            TestGenerationSettings.DEFAULT_OBJENESISPATH));
+            prefix + PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL));
+        setOpenjmlPath(
+            SettingsConverter.read(props, prefix + PROP_OPENJML_PATH, DEFAULT_OPENJMLPATH));
+        setObjenesisPath(SettingsConverter.read(props, PROP_OBJENESIS_PATH, DEFAULT_OBJENESISPATH));
         setIncludePostCondition(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_INCLUDE_POST_CONDITION,
-            TestGenerationSettings.DEFAULT_INCLUDEPOSTCONDITION));
+            PROP_INCLUDE_POST_CONDITION, DEFAULT_INCLUDEPOSTCONDITION));
     }
 
     public boolean removeDuplicates() {
@@ -252,22 +237,56 @@ public boolean useJunit() {
 
     @Override
     public void writeSettings(Properties props) {
-        SettingsConverter.store(props, TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION,
+        var prefix = "[" + CATEGORY + "]";
+        SettingsConverter.store(props, prefix + PROP_APPLY_SYMBOLIC_EXECUTION,
             applySymbolicExecution);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_CONCURRENT_PROCESSES,
-            concurrentProcesses);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_INVARIANT_FOR_ALL,
-            invariantForAll);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_MAX_UWINDS, maxUnwinds);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_OUTPUT_PATH, outputPath);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_REMOVE_DUPLICATES,
-            removeDuplicates);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_USE_RFL, useRFL);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_USE_JUNIT, useJunit);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_OPENJML_PATH, openjmlPath);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_OBJENESIS_PATH, objenesisPath);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_INCLUDE_POST_CONDITION,
-            includePostCondition);
+        SettingsConverter.store(props, prefix + PROP_CONCURRENT_PROCESSES, concurrentProcesses);
+        SettingsConverter.store(props, prefix + PROP_INVARIANT_FOR_ALL, invariantForAll);
+        SettingsConverter.store(props, prefix + PROP_MAX_UWINDS, maxUnwinds);
+        SettingsConverter.store(props, prefix + PROP_OUTPUT_PATH, outputPath);
+        SettingsConverter.store(props, prefix + PROP_REMOVE_DUPLICATES, removeDuplicates);
+        SettingsConverter.store(props, prefix + PROP_USE_RFL, useRFL);
+        SettingsConverter.store(props, prefix + PROP_USE_JUNIT, useJunit);
+        SettingsConverter.store(props, prefix + PROP_OPENJML_PATH, openjmlPath);
+        SettingsConverter.store(props, prefix + PROP_OBJENESIS_PATH, objenesisPath);
+        SettingsConverter.store(props, prefix + PROP_INCLUDE_POST_CONDITION, includePostCondition);
+    }
+
+    @Override
+    public void readSettings(Configuration props) {
+        var cat = props.getSection(CATEGORY);
+        if (cat == null)
+            return;
+        setApplySymbolicExecution(
+            cat.getBool(PROP_APPLY_SYMBOLIC_EXECUTION, DEFAULT_APPLYSYMBOLICEX));
+        setMaxUnwinds(cat.getInt(PROP_MAX_UWINDS, DEFAULT_MAXUNWINDS));
+        setOutputPath(cat.getString(PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH));
+        setRemoveDuplicates(cat.getBool(PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES));
+        setRFL(cat.getBool(PROP_USE_RFL, DEFAULT_USERFL));
+        setUseJunit(cat.getBool(PROP_USE_JUNIT, DEFAULT_USEJUNIT));
+        setConcurrentProcesses(cat.getInt(PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES));
+        setInvariantForAll(cat.getBool(PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL));
+        setOpenjmlPath(cat.getString(PROP_OPENJML_PATH, DEFAULT_OPENJMLPATH));
+        setObjenesisPath(cat.getString(PROP_OBJENESIS_PATH, DEFAULT_OBJENESISPATH));
+        setIncludePostCondition(
+            cat.getBool(PROP_INCLUDE_POST_CONDITION, DEFAULT_INCLUDEPOSTCONDITION));
+    }
+
+    @Override
+    public void writeSettings(Configuration props) {
+        var cat = props.getOrCreateSection(CATEGORY);
+
+        cat.set(PROP_APPLY_SYMBOLIC_EXECUTION, applySymbolicExecution);
+        cat.set(PROP_CONCURRENT_PROCESSES, concurrentProcesses);
+        cat.set(PROP_INVARIANT_FOR_ALL, invariantForAll);
+        cat.set(PROP_MAX_UWINDS, maxUnwinds);
+        cat.set(PROP_OUTPUT_PATH, outputPath);
+        cat.set(PROP_REMOVE_DUPLICATES, removeDuplicates);
+        cat.set(PROP_USE_RFL, useRFL);
+        cat.set(PROP_USE_JUNIT, useJunit);
+        cat.set(PROP_OPENJML_PATH, openjmlPath);
+        cat.set(PROP_OBJENESIS_PATH, objenesisPath);
+        cat.set(PROP_INCLUDE_POST_CONDITION, includePostCondition);
     }
 
     public void set(TestGenerationSettings settings) {

key.core/src/main/antlr4/KeYLexer.g4

@@ -408,8 +408,6 @@ SL_COMMENT
 
 DOC_COMMENT: '/*!' -> more, pushMode(docComment);
 ML_COMMENT: '/*' -> more, pushMode(COMMENT);
-
-
 BIN_LITERAL: '0' 'b' ('0' | '1' | '_')+ ('l'|'L')?;
 
 HEX_LITERAL: '0' 'x' (DIGIT | 'a'..'f' | 'A'..'F' | '_')+ ('l'|'L')?;
@@ -450,7 +448,7 @@ DOUBLE_LITERAL:
     ;
 
 REAL_LITERAL:
-    RATIONAL_LITERAL ('r' | 'R')
+    RATIONAL_LITERAL ('r' | 'R')?
     ;
 
 

key.core/src/main/antlr4/KeYParser.g4

@@ -814,7 +814,8 @@ profile: PROFILE name=string_value SEMI;
 
 preferences
 :
-	KEYSETTINGS LBRACE (s=string_value)? RBRACE
+	KEYSETTINGS (LBRACE s=string_value? RBRACE
+	            |  c=cvalue ) // LBRACE, RBRACE included in cvalue#table
 ;
 
 proofScript
@@ -824,3 +825,23 @@ proofScript
 
 // PROOF
 proof: PROOF EOF;
+
+// Config
+cfile: cvalue* EOF;
+//csection: LBRACKET IDENT RBRACKET;
+ckv: doc=DOC_COMMENT? ckey ':' cvalue;
+ckey: IDENT | STRING_LITERAL;
+cvalue:
+    IDENT #csymbol
+  | STRING_LITERAL #cstring
+  | BIN_LITERAL #cintb
+  | HEX_LITERAL #cinth
+  | MINUS? INT_LITERAL #cintd
+  | MINUS? FLOAT_LITERAL #cfpf
+  | MINUS? DOUBLE_LITERAL #cfpd
+  | MINUS? REAL_LITERAL #cfpr
+  | (TRUE|FALSE) #cbool
+  | LBRACE
+     (ckv (COMMA ckv)*)? COMMA?
+    RBRACE #table
+  | LBRACKET (cvalue (COMMA cvalue)*)? COMMA? RBRACKET #list;