key

key copied to clipboard

TestTacletEquality ignores semantic switches

3

## Description While working on #3353, I noticed that changes inside of semantic switches in taclets are ignored. For example, consider the following taclet: ``` assignmentMultiplicationInt { \find(\modality{#normalassign}{.. #loc =...

WolframPfeifer

Follow-up tasks for overflow checking fix (#3353)

1

## Description This issue contains non-critical follow-up tasks of #3353: * [ ] New Feature: activate the taclet option corresponding to the `code_safe_math`/`code_java_math` annotation * [ ] Documentation: create a...

WolframPfeifer

Re-enable sonarqube for quality assessment

2

## Issue As discussed in the kakey meetting, the current situation of the quality assessment tool is rather unsatisfying. This PR removes the current tools (pmd, checkstyle, qodana, codeql) in...

wadoon

Remove sequent formula

1

## Intended Change This PR prepares the ground for generalizing proof and calculus structures. It removes the superfluous SequentFormula class, which is only a behaviorless container for a term. The...

unp1

Bumps the github-actions-deps group with 2 updates: [gradle/actions](https://github.com/gradle/actions) and [JetBrains/qodana-action](https://github.com/jetbrains/qodana-action). Updates `gradle/actions` from 4.0.1 to 4.1.0 Release notes Sourced from gradle/actions's releases. v4.1.0 This release brings some minor improvements: The...

dependabot[bot]

Isabelle Translation

1

## Related Issue This pull request addresses #. ## Intended Change Adds a plugin, which allows the user to automatically translate a KeY sequent to an Isabelle theory and run...

BookWood7th

## Description While working on some things in `keyext.rusty` I was taking a look at EqualsModProofIrrelevancy in `key.util` to see where it is used and how it works. The test...

tobias-rnh

JavacExtension does not work with classpath/bootclasspath

1

## Description When a .key/.proof file is loaded which contains a `\bootclasspath` directive, the Javac extensions crashes. The bug was originally found by @unp1. ## Reproducible always ### Steps to...

WolframPfeifer

This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1535) where the discussions are preserved. ---- ## Description Currently a proof obligation is created for every block contract in a Java project regardless of...

wadoon

Soundness hole with Contract axiom

1

This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1704) where the discussions are preserved. ---- Using the contract axiom while proving a model method allows to introduce soundness holes. Or am I doing...

wadoon