search

mutilin / klever

Klever Git repository read-only mirror
https://forge.ispras.ru/projects/klever
Apache License 2.0
0 stars 1 forks source link

Posibility to adjust error trace #28

Closed PavelAndrianov closed 5 years ago

PavelAndrianov commented 5 years ago

A verifier may insert notes and warnings incorrectly and it is useful to have an ability to adjust an error trace. Not a converted one, but a visualized one. So, for example, CPALockator highlights now all lock operations. However, only some of them related to a data race. A lot of notes may confuse a developer. So, an expert may adjust the trace, remove all unnecessary locks, maybe, insert a couple of new notes into the trace and then send a link to the trace to a developer. We should think about, how to save relation to the origin trace to be able to apply and modify marks. A possible idea is no have a trace extension, which affects only on visualization and not on marks application. Or, maybe, this extension is helpful for adjusting marks too. Discussion required. A bit related with #18.

vmordan commented 5 years ago

If we modify error trace, then its converted error traces (cached) should be changed along with all corresponding marks application. Maybe, this can be useful at some point, for example, before creating any marks for this error trace, but generally this will be very complex operation. Besides, if we have marks, which were linked directly to modified error trace, they should be completely recalculated, which may change their meanings.

On the other hand, modifying only visualization of the error trace will be much more faster, yet it also may be confusing (for example, if the user removes some note, it still remain in converted error traces).

Therefore, both extensions may be useful.

PavelAndrianov commented 5 years ago

Roughly, we may implement this feature only as 'developer' one. So, its usage may be not very user-friendly, if we consider it should be used only by ourselves. Considering two cases (modify a trace or modify only its visualization), I would say, that we are mostly interested in visualization. So, if we modify the trace itself, the corresponding mark is not applied to similar error traces. That is not what we want. If a traces are similar, the extra information, which is shown to user, should not infer the mark application. Thus, the main use-case, which I see now, is an adjustment of a trace before reporting it to developers. Seems, now they are afraid of our traces and look only on our text description.

vmordan commented 5 years ago

Implemented in commit 7e5d71c.