key icon indicating copy to clipboard operation
key copied to clipboard
verified publisher icon KeYProject

SourceView does not highlight symbolically executed statements (sometimes)

Open unp1 opened this issue 2 years ago • 2 comments

Description

Please describe your concern in detail!

The SourceView seems not too highlight symbolically executed statements in green, if the contract to be proven is inherited.

Reproducible

Is the issue reproducible? Select one of: always, sometimes, random, have not tried, n/a

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

  1. Start KeY
  2. Load Example ...
  3. Select Dynamic Frames > List With Ghosts
  4. Choose method add and start proof
  5. Symbolically statements of add are not highlighted

What is your expected behavior and what was the actual behavior?

Additional information

Add more details here. In particular: if you have a stacktrace, put it here.

  • Commit: f9f3fff (also KeY 2.12.1)

unp1 avatar Nov 07 '23 21:11 unp1

  • I could not reproduce the bug on my computer (commit c0eca7725ce4b77aedcf2d35d26f5f5e08d845de, manjaro linux).
  • @flo2702 reproduced it (same commit, ubuntu linux).

lks9 avatar Feb 19 '25 15:02 lks9

We suspect it has something to do with drawing in normal threads instead of swing threads (concurrency bug).

lks9 avatar Feb 20 '25 08:02 lks9