WitnessLinter ignores threads when checking callstack validity.
Created by: kfriedberger
The current witnesslinter only checks callstack validity for sequential programs and does not consider thread interleaving. This could lead to marking valid witnesses as invalid. I have not tested the behaviour, this issue is only based on a quick code review.
The concurrent tasks of the current SV-COMP are simple enough and do (hopefully) not use more than one function call per thread. Thus, this problem is not urgent, but should be solved until next year.
As threadids are optional, the following sequence of transitions is valid:
- enter foo - enter bar - return from foo - return from bar
With threadIds, the same sequence could be written as
- threadId=0, enter foo - threadId=1, enter bar - threadId=0, return from foo - threadId=1, return from bar