Fix handling of \values keyword

[FliegendeWurst]

Related Issue

This pull request resolves #3717.

Intended Change

Fix by always using the type for Seq, not the type of the containing class.

Plan

• Add a simple test case for usage of \values

Type of pull request

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

Ensuring quality

• I have tested the feature as follows: a file with \values now loads a bit further (see Enhanced-for loop example with \values not loadable #3717 (comment))

Additional information and contact(s)

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

[codecov]

Codecov Report

❌ Patch coverage is 0% with 10 lines in your changes missing coverage. Please review.
✅ Project coverage is 47.97%. Comparing base (2aa39bb) to head (790b0ce).
⚠️ Report is 51 commits behind head on main.

Files with missing lines	Patch %	Lines
...ava/de/uka/ilkd/key/speclang/LoopContractImpl.java	0.00%	7 Missing ⚠️
.../de/uka/ilkd/key/speclang/njml/JmlTermFactory.java	0.00%	2 Missing ⚠️
...java/de/uka/ilkd/key/speclang/njml/Translator.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3718      +/-   ##
============================================
- Coverage     47.99%   47.97%   -0.02%     
- Complexity    16046    16055       +9     
============================================
  Files          1683     1683              
  Lines         96044    96099      +55     
  Branches      15387    15401      +14     
============================================
+ Hits          46093    46107      +14     
- Misses        44681    44716      +35     
- Partials       5270     5276       +6     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[WolframPfeifer]

@flo2702 Can you take a look here? I think you were involved at some time in the implementation of foreach loops ...

[flo2702]

I just pushed some fixes, which allow the proofs to load further. They still don't close automatically, but this may be due to errors in the spec or just the difficulty in the proofs. @FliegendeWurst Maybe you can take another look at it now.

@unp1 I removed some assert false statements in JavaDLTheory that lead to an assertion failure every time a \values expression is parsed. git blame says that you wrote that class, and I don't entirely understand what it does, so is this right?

[unp1]

Hi,

@unp1 I removed some assert false statements in JavaDLTheory that lead to an assertion failure every time a \values expression is parsed. git blame says that you wrote that class, and I don't entirely understand what it does, so is this right?

fine to remove them. The idea was more that JavaDLTheory should never be asked whether it is responsible for literals etc. But that was not a valid thought :-) and it should just return false.