search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
44 stars 25 forks source link

complex JML storerefs cannot be parsed #1459

Open wadoon opened 1 year ago

wadoon commented 1 year ago

This issue was created at git.key-project.org where the discussions are preserved.

## Description More complex JML storerefs like `array[*].field` cannot be parsed by KeY though they are (allegedly) valid JML. ## Reproducible always ### Steps to reproduce See attached bug report. ### Additional information This has been reported by Jan Boerman via the KeY feedback functionality.[key-bugreport2113557284245157491.zip](/uploads/4cbabd394ebb750ebcfb6903c315382b/key-bugreport2113557284245157491.zip) The workaround is to write the KeY specific expression `\infinite_union(int i; 0<=i&&i

Information:

  • created_at: 2018-01-10T09:53:35.295Z
  • updated_at: 2018-01-10T09:53:35.295Z
  • closed_at: None (closed_by: )
  • milestone:
  • user_notes_count: 0
FliegendeWurst commented 1 year ago

Similar to #992