Anonymize ghost variables in loop

[Drodt]

Related Issue

This pull request resolves #3720.

Intended Change

(Ghost) set statements are now considered for the set of to-be-anonymized variables for loop scope rules.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code

Ensuring quality

• I added new test case(s) for new functionality.
• I have tested the feature as follows: Tested example from Ghost variable not properly handled in loop #3720

Additional information and contact(s)

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

[Drodt]

Open questions for this PR:

• Should I move the test file to a different folder?
• Should I also create a .key file for the loop transform rule? (I tested it manually and both use the same method to get the written to variable, which are then anonymized)

[FliegendeWurst]

I have tested this change a bit and it seems to work well. 👍

[WolframPfeifer]

Thanks, this indeed solves the problem also in the case study where it occurred.

For your questions:

• Since the other tests also seem to read from that folder, I think we can keep it like that for now.
• Since both loop rules use the same function here, I think it is not beneficial to have a second test. It might, however, be a good idea to do a more fine-grained test which only tests the method in MiscTools without loading the taclets, create the environment etc. (i.e. a proper unit test).

[WolframPfeifer]

@Drodt I approved, but maybe you can check my comment regarding the unit test and merge depending on your opinion ...

[Drodt]

* Since both loop rules use the same function here, I think it is not beneficial to have a second test. It might, however, be a good idea to do a more fine-grained test which only tests the method in MiscTools without loading the taclets, create the environment etc. (i.e. a proper unit test).

Good idea; I'll look into it next week (hopefully)