Handle Switch in Taclets w/o Transformer

[Drodt]

Intended Change

Instead of relying on the switch-to-if transformer, which may have some bugs, this PR attempts to handle switch statements purely in taclets.

The general approach is to mark the branch currently executed as the active-case.

Effect on Proofs

Name	Nodes (main)	Nodes (match-switch)	Nodes Diff	Branches (main)	Branches (match-switch)	Branches Diff
examples/standard_key/java_dl/switch/empty_switch_array_out_of_bounds_catch.key	275	250	-25	149	143	-6
examples/standard_key/java_dl/switch/large_switch.key	4410	3642	-768	2682	2478	-204
examples/standard_key/java_dl/switch/switch_in_switch.key	5215	2031	-3184	4376	1583	-2793
examples/standard_key/java_dl/switch/empty_switch_null_catch.key	308	275	-33	106	92	-14
examples/standard_key/java_dl/switch/empty_switch_array_out_of_bounds.key	398	372	-26	179	172	-7
examples/standard_key/java_dl/switch/while_and_switch.key	1237	1261	24	831	884	53
examples/standard_key/java_dl/switch/empty_switch_null.key	237	204	-33	79	65	-14
examples/standard_key/java_dl/switch/empty_switch.key	8	3	-5	9	4	-5
examples/standard_key/java_dl/switch/labeled_case.key	194	153	-41	86	82	-4

Plan

• Finish implementation

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• 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
• Other:

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.
• For new Gradle modules: I added the Gradle module to the test matrix in
  .github/workflows/tests.yml

Additional information and contact(s)

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

[wadoon]

I have looked into your commit. You have violated some principles of the javaparser: The AST class was not registered in ALL_NODE_CLASSES. This will lead to further reconstructions.

Also, we should avoid keywords with minuses.
https://github.com/wadoon/key-javaparser/blob/5ed28cb6c6bbab77d8ad47d5a02d6ab180354527/javaparser-core/src/main/javacc/java.jj#L5079C1-L5079C59

My first question is: Do we really need a special case for marking the active one? Should we not mark the statements/expression instead? (Active statement vs. inactive prefix)

[wadoon]

I also moved the development to https://github.com/jmltoolkit/jmltk

Repo wadoon/key-javaparser is obsolete.

[Drodt]

I have looked into your commit. You have violated some principles of the javaparser: The AST class was not registered in ALL_NODE_CLASSES. This will lead to further reconstructions.

Alright. fixed.

Also, we should avoid keywords with minuses. https://github.com/wadoon/key-javaparser/blob/5ed28cb6c6bbab77d8ad47d5a02d6ab180354527/javaparser-core/src/main/javacc/java.jj#L5079C1-L5079C59

I'm fine with activecase or activeCase.

My first question is: Do we really need a special case for marking the active one? Should we not mark the statements/expression instead? (Active statement vs. inactive prefix)

I see no other way to mark that we are currently executing a switch entry. Other ways like moving statements out of the switch do not model fall through semantics.