From bfbe83791367823d1c1a889fa70869bd6037f49b Mon Sep 17 00:00:00 2001
From: Karlheinz Friedberger <kfriedberger@gmail.com>
Date: Tue, 8 Dec 2020 13:47:22 +0100
Subject: [PATCH] add tracking of existing threadIds and threadCreations.

---
 lint/witnesslint/linter.py  | 7 +++++++
 lint/witnesslint/witness.py | 2 ++
 2 files changed, 9 insertions(+)

diff --git a/lint/witnesslint/linter.py b/lint/witnesslint/linter.py
index e054e4a..0ce23ec 100644
--- a/lint/witnesslint/linter.py
+++ b/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()
diff --git a/lint/witnesslint/witness.py b/lint/witnesslint/witness.py
index 6a92519..dfafbdb 100644
--- a/lint/witnesslint/witness.py
+++ b/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 = {}