Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix newnames handling for new local vars #3438

Merged
merged 3 commits into from
Apr 20, 2024

Conversation

FliegendeWurst
Copy link
Member

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

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

Ensuring quality

Additional information and contact(s)

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

Copy link

codecov bot commented Mar 7, 2024

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 ⚠️
...n/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java 0.00% 6 Missing ⚠️
.../main/java/de/uka/ilkd/key/proof/NameRecorder.java 75.00% 1 Missing ⚠️
Additional details and impacted files
@@             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              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@FliegendeWurst
Copy link
Member Author

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.

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this PR is fine, apart from my small comment about the constant name.

@mattulbrich
Copy link
Member

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

@wadoon wadoon added this pull request to the merge queue Apr 20, 2024
Merged via the queue into KeYProject:main with commit 18cca64 Apr 20, 2024
13 of 14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Simple Java program with array creation cannot be sliced
4 participants