key icon indicating copy to clipboard operation
key copied to clipboard

Solving the FP completeness issues in #1723

Open mattulbrich opened this issue 2 years ago • 9 comments

Related Issue

This pull request answers to issue #1723.

Intended Change

Floats and doubles are currently incorrectly insufficiently handled when they appear in one expression.

Casts need to be added and casts need to be dealt with. ...

  • [x] introducing casts where needed
  • [ ] adding rules / SMT support for such casts.

Type of pull request

  • [x] Bug fix (non-breaking change which fixes an issue)
  • [x] 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)
  • [x] There are changes to the (Java) code
  • [x] There are changes to the taclet rule base
  • [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
  • [ ] Other:

Ensuring quality

  • [x] I made sure that introduced/changed code has been well documented (javadoc).
  • [x] I added new test case(s) for new functionality.
  • [x] I have tested the feature as follows: small 2-liners
  • [ ] I have checked that runtime performance has not deteriorated

Additional information and contact(s)

It's still W I P.

@samysweb

The contributions within this pull request will be licensed under GPL2-or-later wihtin KeY.

mattulbrich avatar Feb 05 '23 15:02 mattulbrich