ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
threading.Thread Class Reference

Public Member Functions

None __init__ (self)
None start (self)
None join (self)

Protected Attributes

int _tid = 0

Detailed Description

Skeleton matching ``threading.Thread``.

Constructor takes no parameters: the AST pre-pass strips
``target=``/``args=`` from every Thread construction before the
Python frontend reaches this class, so the skeleton only has to
exist as a placeholder. ``start()``/``join()`` are likewise
rewritten by ``lower_threading_thread_usage`` and never invoked
on this skeleton in well-formed programs.

The method bodies assert ``False`` to make any path that *does*
reach them — e.g. a dynamic-lookup escape such as
``Cls = threading.Thread; Cls()`` that the validator did not see
— fail loudly with a verification assertion rather than silently
skipping the spawn.

Constructor & Destructor Documentation

◆ __init__()

None threading.Thread.__init__ ( self)

Member Function Documentation

◆ join()

None threading.Thread.join ( self)
Reached only when the AST rewrite failed to lower a Thread.

◆ start()

None threading.Thread.start ( self)
Reached only when the AST rewrite failed to lower a Thread.

Member Data Documentation

◆ _tid

int threading.Thread._tid = 0
protected

The documentation for this class was generated from the following file: