Add test for Java parsing coverage#3916
Merged
Merged
Conversation
unp1
force-pushed
the
java-coverage-parsing-tests
branch
from
July 11, 2026 23:40
153641e to
d96609f
Compare
unp1
force-pushed
the
java-coverage-parsing-tests
branch
from
July 11, 2026 23:56
d96609f to
877ea2c
Compare
Member
|
Would it not be nice to confirm this via |
Member
Author
|
Not sure I can follow. How would you use Jacoco to measure how much Java constructs are supported by KeY? Measuring how many visit/listener methods are executed? |
Member
You can measure the coverage quantitatively by |
wadoon
approved these changes
Jul 13, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Intended Change
This PR adds 48 test cases for Java constructs that are parser supported (it is not checked whether KeY can deal with them on a calculus level).
The tests record the current status quo, this means they fail when a supported construct can no longer be supported and they fail if a construct becomes supported (in the latter case the error message says to change the test case to refelct that a new feature is supported)
One thing that stands out is that we can parse
var x = 0;if the right-hand side is a primtiive type but something with a reference typevar x = "hi";fails.The tests are an artifact of determining the Java coverage for KeY 3.0 (see https://keyproject.github.io/key-docs/user/SupportedFeatures/JavaCoverage/)
Type of pull request
Ensuring quality
Additional information and contact(s)
Created with AI tooling suuport
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.