completeness gap for array types

[wadoon]

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

---

Description

Amongst others, the term o.f(at)heap + 1 is parsed incorrectly

Reproducible

always

Steps to reproduce

Create A.java:

class A { int f; }

Create a.key (in same directory):

\javaSource ".";

\programVariables { A that; }

\problem { that.f(at)heap + 1 = 1 + that.f(at)heap }

Load it. KeY fails.

This file can be loaded into %"v2.8.0" however.

Additional information

Another problem is that the error message is pretty broken and does not allow to browse the guilty source code:
Could not build term on: heap+1/tmp/k/a.key:6:18

---

• Commit: bee2f7f582f39c914b5f11725aa1eb115233fde8, master at the time

---

Information:

• created_at: 2021-04-28T23:54:57.827Z
• updated_at: 2022-01-21T16:35:32.131Z
• closed_at: 2021-05-06T07:34:11.814Z (closed_by: mulbrich)
• milestone:
• user_notes_count: 2