add tracking of existing threadIds and threadCreations.

lint/witnesslint/linter.py

@@ -32,6 +32,8 @@
 NO_PROGRAM = 6
 INTERNAL_ERROR = 7
 
+MAIN_THREAD_ID = '0'
+
 
 def create_linter(argv):
     arg_parser = create_arg_parser()
@@ -446,6 +448,7 @@ def handle_edge_data(self, data, key, parent):
                     break
             self.check_functionname(data.text, data.sourceline)
         elif key == witness.THREADID:
+            self.witness.thread_ids.add(data.text)
             # 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
@@ -456,6 +459,7 @@ def handle_edge_data(self, data, key, parent):
             #     )
             pass
         elif key == witness.CREATETHREAD:
+            self.witness.thread_creations.add(data.text)
             if data.text in self.witness.threads:
                 # logging.warning(
                 #     "Thread with id {} has already been created".format(data.text),
@@ -868,6 +872,9 @@ def final_checks(self):
                 collections.OrderedDict(sorted(self.witness.transitions.items())),
                 self.witness.entry_node,
             )
+        spare_thread_ids = self.witness.thread_ids - self.witness.thread_creations - set(MAIN_THREAD_ID)
+        if spare_thread_ids:
+            logging.warning("Threads were executed, but never created: {}".format(spare_thread_ids))
         if self.program_info is not None:
             for check in self.check_later:
                 check()

lint/witnesslint/witness.py

@@ -108,6 +108,8 @@ def __init__(self, witness_file):
         self.defined_keys = {}
         self.used_keys = set()
         self.threads = {}
+        self.thread_creations = set()
+        self.thread_ids = set()
         self.transition_sources = set()
         self.transitions = {}