Fix #3524

[Drodt]

Related Issue

This pull request addresses #3524.

Intended Change

For all loopScopeInv rules: Declares for each local variable i a new PV i_before, stores the value of i before the loop in i_before, and applies {i := i_before} to the frame condition.

Type of pull request

• Bug fix: Breaking-Change (existing proofs with loops might no longer load)
• 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 bas

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: Some local tests, including the example of Soundness bug: Assignable treatment is wrong #3524.
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

Thanks @unp1!

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

[mattulbrich]

Guys, ... you are quick! 👏 @Drodt @unp1

[github-actions]

Qodana Community for JVM

It seems all right 👌

No new problems were found according to the checks applied

💡 Qodana analysis was run in the pull request mode: only the changed files were checked

View the detailed Qodana report

To be able to view the detailed Qodana report, you can either:

• Register at Qodana Cloud and configure the action
• Use GitHub Code Scanning with Qodana
• Host Qodana report at GitHub Pages
• Inspect and use qodana.sarif.json (see the Qodana SARIF format for details)

To get *.log files or any other Qodana artifacts, run the action with upload-result option set to true,
so that the action will upload the files as the job artifacts:

      - name: 'Qodana Scan'
        uses: JetBrains/qodana-action@v2024.2.3
        with:
          upload-result: true

Contact Qodana team

Contact us at qodana-support@jetbrains.com

• Or via our issue tracker: https://jb.gg/qodana-issue
• Or share your feedback: https://jb.gg/qodana-discussions

[mattulbrich]

It seems that the fix requires a larger change on the loop rule. There seem to be new "_Before" variables now. But ... are there not already _Before-Variables available on the sequent?

[Drodt]

It seems that the fix requires a larger change on the loop rule. There seem to be new "_Before" variables now. But ... are there not already _Before-Variables available on the sequent?

Not necessarily for possibly modified local variables wrt. the loop scope rule. The old loop rule did add those variables, the loop scope rule does not.

[mattulbrich]

Loooks a lot cleaner without the maps in the schema variable. Thanks