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

Support intersecting threaded error traces in MEA #51

Open vmordan opened 5 years ago

vmordan commented 5 years ago

Currently MEA supports only error traces, in which threads do not intersect. At the same time, error trace may switch between several threads: thread-1: ... thread-2: ... thread-1: ... thread-2: ... In order to support such error traces, MEA format should be extended.

vmordan commented 1 year ago

@PavelAndrianov Is this issue still relevant? If yes, do we have any examples of such witnesses?

PavelAndrianov commented 1 year ago

Actually, do not remember the case, where it was needed. Moreover, CPALockator outputs not intersected traces.