Improve enforcement of Java AST immutability #4
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
unp1
commented
Oct 21, 2023
unp1
commented
- The program variable replacer also needs to consider lefthandside's of elementary updates
- Avoid collisions with names occurring in the namespace (and not only inside programs)
- Introduce new program variables properly in loop invariant rules
- Minor clean ups
- Some codestyle cleanups
- Fix taclet equality tests
- Fix copy-paste error in modified rules
- Fix failing test.
- Some fixes for test cases and cleanup (+1 squashed commit)
- Fixed broken proofs
- Fix slicing tests
- updating GenerateUnitTests to Java 17+
- further code refactorings
- further refactorings
- further refactorings
- reformat
- SMT: add Z3_QF variant
- gradle: specify inputs and outputs of tasks
- Bump com.miglayout:miglayout-swing from 11.1 to 11.2
- Some general minor code quality improvements
- spotless fixes
- Fix error behavior during proof saving
- SMT: tweak Z3_QF description wording
- Remove invalid JavaDoc refering to not thrown exceptions
- JavaDoc @throws fixes
- Update beanshell to 2.0b6 which includes a fix for a security vulnerability
- add metadata for POM generation and update templates for license headers
- bugfix: KeY files with errors cannot be edited.
- spotless: adding a space
- Statistics constructor from node list
- Proof macro: record statistics correctly
- Fully disable origin tracking if it is disabled
- Disable stop button once it is used
- Keep strategy info visible after applying
- Fix environments not disposed in tests
- Fix unit test
- Kill SMT solvers properly on timeout
- Fix gradle detection of git branch
- Fix rare edge case in dependency analyzer
- Fix branch selection in caching
- Fix proof tree behaviour when toggling goals
- Remove AutoClosable on KeYEnvironment
- Update build.gradle
- Fix wrong quicksave failed warning
- spotless warning
- Update nightlydeploy.yml
- Update .github/workflows/nightlydeploy.yml
- Make fields in Sort and Term final. Restore package private visibility of TemrImpl
- spotless fixes
- Fix for issue displayname of Taclets need to be free of spaces. KeYProject/key#3286: Parsing of rule display names that contain spaces in origin labels
- Regression test for fixed issue displayname of Taclets need to be free of spaces. KeYProject/key#3286
- Stricter enforcement of Java AST immutability
…f elementary updates
This will cause saved proofs to break
* Dead code * Typos
* switch expression * Files.writeString
* switches * code clean up
This way the solvers.txt will automatically be regenerated.
Bumps [com.miglayout:miglayout-swing](https://github.com/mikaelgrev/miglayout) from 11.1 to 11.2. - [Release notes](https://github.com/mikaelgrev/miglayout/releases) - [Changelog](https://github.com/mikaelgrev/miglayout/blob/master/release.txt) - [Commits](mikaelgrev/miglayout@v11.1...v11.2) --- updated-dependencies: - dependency-name: com.miglayout:miglayout-swing dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] <[email protected]>
Refactoring and Code clean up. * switch statements into switch expression where it was useful. (avoids fall throughs and often more compact code) * some smaller (non-structured) clean ups * ensure camel cases variable names * fix Javadoc * and other code smells recognize by IntelliJ
Bumps [com.miglayout:miglayout-swing](https://github.com/mikaelgrev/miglayout) from 11.1 to 11.2. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/mikaelgrev/miglayout/releases">com.miglayout:miglayout-swing's releases</a>.</em></p> <blockquote> <h2>Release v11.2</h2> <h2>Changelog</h2> <p>59eb209 Merge pull request <a href="https://redirect.github.com/mikaelgrev/miglayout/issues/100">#100</a> from vlsi/ci_for_prs</p> <p>chore: excute CI tests in PRs bf1c1b9 chore: excute CI tests in PRs 1396476 fix warnings 598ab3e Merge pull request <a href="https://redirect.github.com/mikaelgrev/miglayout/issues/96">#96</a> from vlsi/deprecations</p> <p>Fix Java deprecations 94bd9cc style: replace deprecated getConstaints with getConstraints beaf337 style: replace deprecated setConstaints with setConstraints f299032 style: suppress generic array creation warning in LinkHandler 2a550af deprecation: replace new Float(x) with autoboxing 3f139f1 chore: add -Werror and -Xlint:all Java compiler options 36e1780 chore: make mvnw executable 90875f6 added error-prone to prevent toLowerCase() issues 39ab4d5 toLowerCase either needs hardcode text or use Locale.ROOT because of Locale (tr_TR) issues 341e16b adding stongly typed methods for common usages c37e39c to 11.2-SNAPSHOT 657123c remove release profile 18bcfbe trying to overwrite github 4fb63a8 attempting to release 11.1</p> </blockquote> </details> <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/mikaelgrev/miglayout/commit/59eb2091bf7a9cfe01b07dc096e53f994b290516"><code>59eb209</code></a> Merge pull request <a href="https://redirect.github.com/mikaelgrev/miglayout/issues/100">#100</a> from vlsi/ci_for_prs</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/bf1c1b95db2ffec59098e8a153b1ef1c6a8cb63c"><code>bf1c1b9</code></a> chore: excute CI tests in PRs</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/1396476ffc6100c5352db5cc83134861593360a5"><code>1396476</code></a> fix warnings</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/598ab3e392d57783eebc3e043f2efea55390b117"><code>598ab3e</code></a> Merge pull request <a href="https://redirect.github.com/mikaelgrev/miglayout/issues/96">#96</a> from vlsi/deprecations</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/94bd9ccc393894007647f4b3db85e7331e9cf13a"><code>94bd9cc</code></a> style: replace deprecated getConstaints with getConstraints</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/beaf33773ee576af8a504a1cf768596cc2da485e"><code>beaf337</code></a> style: replace deprecated setConstaints with setConstraints</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/f299032b9766691582b24e1873f0cc97e30efb7f"><code>f299032</code></a> style: suppress generic array creation warning in LinkHandler</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/2a550af76acd3d6d2b2a94ef50aefa53f0f83ea1"><code>2a550af</code></a> deprecation: replace new Float(x) with autoboxing</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/3f139f180dd839dd7ac430a97d625e95bedfe810"><code>3f139f1</code></a> chore: add -Werror and -Xlint:all Java compiler options</li> <li><a href="https://github.com/mikaelgrev/miglayout/commit/36e17809be31aee89018bbac05f0a03a6cb82842"><code>36e1780</code></a> chore: make mvnw executable</li> <li>Additional commits viewable in <a href="https://github.com/mikaelgrev/miglayout/compare/v11.1...v11.2">compare view</a></li> </ul> </details> <br /> [](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) --- <details> <summary>Dependabot commands and options</summary> <br /> You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show <dependency name> ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself) </details>
…to minorCodeFixes
Might be added again later if we agree on its usefulness.
Fix for issue #3158 - The program variable replacer also needs to consider lefthandside's of elementary updates - Avoid collisions with names occurring in the namespace (and not only inside programs) - Introduce new program variables properly in loop invariant rules - Minor clean ups
The issues were:
* these unnecessary double declarations like
for (T x: y) {
var z = x;
....
}
fixed manually.
* reducing complexity of some very few if statements by switching the
then-and-else branches (fixed automatically, but automatic fix triggered
for each case manually)
* declared but never thrown exceptions (manual fixes)
* some typos in comments I encountered while fixing (manual fixes)
Co-authored-by: Wolfram Pfeifer <[email protected]>
Backporting the bug fixes in KEY-2.12.1 to main. This PR supersedes #3251 to avoid merge conflicts due to file header changes. Necessary changes were cherry-picked.
Quicsave always displayed a failed warning, een in success cases.wq
Setting an explicit Java version for the deployment
Co-authored-by: Wolfram Pfeifer <[email protected]>
Setting an explicit Java version for the deployment
…s in origin labels
…s in origin labels (#3306)
…rm and sorts (#3304) This PR makes TermImpl package private again (no entity outside of de....logic should see an actual implementation). Further the PR strengthens the design decision of terms and sorts being immutable by making fields final and eliminating setters.
|
This PR is not for here. See github.com/keyproject |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.