diff --git a/README.md b/README.md index bc27426..ee7fe7a 100644 --- a/README.md +++ b/README.md @@ -76,8 +76,8 @@ The following information should additionally be available in the witness: | key | Meaning | Allowed in Violation Witnesses | Allowed in Correctness Witnesses | | --- | --- | ---- | ---- | -| threadId | Represents the currently active thread for the transition. If no ``threadId`` is given, any thread can be active. The value should be a unique identififer for a thread. | Yes | Yes | -| createThread | The currently active thread (value of ``threadId``) creates a new thread (value of ``createThread``) . In general, using a ``threadId`` is only allowed after creating a matching thread. The new thread's function can be entered on a second transition following this transition, such that the transition with the ``enterFunction`` key has the ``threadId`` of the created thread. When the function of the thread is exited, the thread is assumed to be terminated and its ``threadId`` should no longer be used. | Yes | Yes | +| threadId | Represents the currently active thread for the transition. The initially active thread has id ``0``. If no ``threadId`` is given, any thread can be active. The value should be a unique identififer for a thread. | Yes | Yes | +| createThread | The currently active thread (value of ``threadId``) creates a new thread (value of ``createThread``) . In general, using a ``threadId`` is only allowed after creating a matching thread, except for thread ``0``, which exits by virtue of starting the program. The new thread's function can be entered on a second transition following this transition, such that the transition with the ``enterFunction`` key has the ``threadId`` of the created thread. When the function of the thread is exited, the thread is assumed to be terminated and its ``threadId`` should no longer be used. | Yes | Yes | CPAchecker partially supports the validation of violation witnesses for concurrent programs. This witness specification and the validator are a work in progress and will be subject to modifications. diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py index fa9ed77..80a62a4 100644 --- a/lint/witnesslint/linter.py +++ b/lint/witnesslint/linter.py @@ -124,6 +124,7 @@ def __init__(self, witness, program, options): self.correctness_witness_only = set() self.check_existence_later = set() self.check_later = [] + self.witness.threads['0'] = None def collect_program_info(self, program): """ @@ -440,15 +441,11 @@ def handle_edge_data(self, data, key, parent): break self.check_functionname(data.text, data.sourceline) elif key == witness.THREADID: - # Check disabled for SV-COMP'21 as questions about the specification - # need to be resolved first, see - # https://gitlab.com/sosy-lab/sv-comp/archives-2021/-/issues/30 - # if data.text not in self.witness.threads: - # logging.warning( - # "Thread with id {} doesn't exist".format(data.text), - # data.sourceline, - # ) - pass + if data.text not in self.witness.threads: + logging.warning( + "Thread with id {} doesn't exist".format(data.text), + data.sourceline, + ) elif key == witness.CREATETHREAD: if data.text in self.witness.threads: logging.warning(