KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Fix newnames handling for new local vars #3438

Closed FliegendeWurst closed 4 months ago

FliegendeWurst commented 5 months ago

Related Issue

This pull request fixes #3437.

Intended Change

Previously, the names of certain local variables were derived using a counter. Now they will also be stored in the name proposals, making it possible to replay their exact value.

Type of pull request

Ensuring quality

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

codecov[bot] commented 5 months ago

Codecov Report

Attention: Patch coverage is 25.00000% with 18 lines in your changes are missing coverage. Please review.

Project coverage is 37.89%. Comparing base (cde763f) to head (5d0d9fc).

Files Patch % Lines
...ilkd/key/rule/metaconstruct/InitArrayCreation.java 0.00% 11 Missing :warning:
...n/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java 0.00% 6 Missing :warning:
.../main/java/de/uka/ilkd/key/proof/NameRecorder.java 75.00% 1 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3438 +/- ## ============================================ + Coverage 37.88% 37.89% +0.01% - Complexity 17082 17090 +8 ============================================ Files 2090 2090 Lines 127485 127504 +19 Branches 21466 21471 +5 ============================================ + Hits 48294 48324 +30 + Misses 73285 73274 -11 Partials 5906 5906 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

FliegendeWurst commented 5 months ago

I don't understand the test failure:

Failed to map supported failure 'org.opentest4j.AssertionFailedError: Wrong result ==> expected: de.uka.ilkd.key.logic.Sequent@5b5e79e7<[]==>[\<{
  {
    {}
  }
  {
    {
      break;
    }
  }
}\> (true)]> but was: de.uka.ilkd.key.logic.Sequent@4170b9f1<[]==>[\<{
  {
    {}
  }
  {
    {
      break;
    }
  }
}\> (true)]>' with mapper 'org.gradle.api.internal.tasks.testing.failure.mappers.OpenTestAssertionFailedMapper@77818d20': Cannot invoke "Object.getClass()" because "expectedValue" is null

> Task :key.core:test
FAILURE: de.uka.ilkd.key.rule.TestApplyTaclet#testBugEmptyBlock()

I'll try to push again.

mattulbrich commented 4 months ago

Does this also fix #3455 where a method parameter length shadows the length function for array length?