Fix model fields resolution when multiple heaps present#3923
Conversation
cd4e9a4 to
bae26a4
Compare
bae26a4 to
6f3e430
Compare
Discovered when trying to specify Throwable using model fields. Model fields (w/o represents or accessible clause) could not be used as they were not resolvable.
6f3e430 to
de20391
Compare
| heapLDT.getFieldSymbolForPV((LocationVariable) attribute, services); | ||
| JTerm attributeTerm; | ||
| if (attribute.isStatic()) { | ||
| if (attribute.isModel()) { |
There was a problem hiding this comment.
Does this not depend on no_state and two_state modifiers?
There was a problem hiding this comment.
do they exist for model fields too? I though just for model methods. Otherwise, I look into that and thanks for bringing it up
There was a problem hiding this comment.
mhm... On the other side, are we not modelling "model fields" using "model methods"?
There was a problem hiding this comment.
The fix is not 3.0 critical. I have a look into it and will not merge before that is setlled. I'll discuss it with Mattias (he knows model fields/methods best, I think) on Friday at the KeY meeting. In principle, the translation is at least similar and if not should be made identical. But I am not sure whether model fields should be allowed to use the modifiers (from a usage point of view).
2 participants
Intended Change
Model fields without a represents or accessible clause could not be used in JavaRedux
as permissions could not build the term (wrong arity).
Found out when trying to specify addSuppressed in Throwable of PR #3918.
This PR should fix it.
Type of pull request
Ensuring quality
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.