Closed fab918 closed 2 months ago
Hi fab918, thanks for the report.
Try adding //@ assignable \nothing;
to the loop specification (like above decrease
).
That should help.
@mattulbrich Thanks for your quick response.
I had tried the JML annotations loop_modifies
and loop_writes
but I had an error message in the import, I understood that it was not supported.
But yes it works with assignable
, however it's not a JML standard, I just saw in the JML reference that it mentions that KeY uses assignable for loop.
Why isn't there an alias for loop_modifies
, loop_writes
, in order to be compatible with JML? It is kind of a shame not being able to have a common code for such a basic functionality when all it would take is an alias.
I had implemented such an alias some years ago, but apparently this did not survive the release cycles. Shouldn't be a problem to reintroduce it though, in my opinion.
@mi-ki Is there any trace of your contribution? I did a search on PRs but I don't see it.
@fab918 I just took a look, but found out I did not introduce an alias for loop_modifies
or loop_writes
, but for loop_variant
and assigns
(yet another standard from somewhere else, apparently). This was commit af97f72d1994cb50c74eb04c77649f198236f8ec. However, I am not sure whether their translation still works as it used to do, since many hard-to-follow things happened to the parser in-between.
@mi-ki Thanks, unfortunately I don't think it always works.
If anyone has any advice on how to get started, I'd love to hear it.
@fab918 I created a new branch which should hopefully fix the previously lost changes and also add the two keywords from OpenJML. Maybe, you can test whether it works for you?
It's been a while and after various internal discussions, the PR #3365 made it onto the main branch. So, @fab918, if you are still around, feel free to use it!
Description
When I use "assignable" in the Key Editor, I have my proof which fails, yet the method does not modify anything. If assignable is removed, it works. This doesn't seem to limit to "\nothing", if I put array or array[*] it still doesn't work.
(I take advantage of this, is it possible to have more information on what is not working? I did not find any information on this subject, it is not clear where the problem lies)
Reproducible
yes
Steps to reproduce
pass the test