Wolfram Pfeifer
Wolfram Pfeifer
## Description The exact dynamic type of arrays of primitive values are always known. However, KeY is missing a rule here. There are also some real world cases, where the...
## Idea At the moment, there are two places where the taclet options can be set: 1. The old dialog: "Options" -> "Show Taclet Options":  2. The newer unified...
## Idea At the moment, during the automatic proof search the GUI of KeY "freezes", i.e. does not respond to input events except for a click on the stop button....
## Description If a generic sort is used inside a problem definition (in a .key file), this leads to a broken sequent. ## Reproducible always ### Steps to reproduce Load...
The purpose of this PR is to repair the overflow checking of KeY and thus fix #3352. TODO: * [x] fix creation of branches for overflow checking * [x] fix...
## Description In the current version of KeY, the integer semantics with explicit overflow checks as introduced by #3027 are broken on at least 3 levels: 1) The annotation `/*@...
## Description When you try to start a proof of a dependency contract of a model field that contains `\strictly_nothing`, an exception is thrown during generation of the proof obligation....
## Description This pull request addresses #3501. Since this a warning (or better, lots of them) that potentially confuses the users, this very minor PR decreases the log level from...
## Description When KeY is started, there are multiple warnings about duplicate sort declarations in the taclet base. While we should get rid of those in the future, they are...
## 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 =...