|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Protected Member Functions | |
| _record_numpy_import (self, node) | |
| _numpy_constructor_name (self, node) | |
| _bind_numpy_constructor_call (self, node) | |
| _bind_numpy_parameters (self, name, node) | |
| _spell_numpy_constructor_call (self, name, node, bound) | |
| _is_pure_numpy_argument (cls, node) | |
| _unpacked_linspace_call (self, node) | |
| _split_linspace_retstep (self, node) | |
| _retstep_bound_arguments (self, call) | |
Static Protected Member Functions | |
| _bind_arange_stop (node, bound) | |
| _reads_unpacked_target (node, bound) | |
| _linspace_step (bound, div) | |
Static Protected Attributes | |
| dict | _NUMPY_CONSTRUCTOR_SIGNATURES |
| dict | _NUMPY_REQUIRED_PARAMS |
Spell a NumPy constructor call in the one form the frontend reads. The frontend reads the leading value parameters of a constructor positionally and the others as keywords. Binding them here gives every reader the same call; a call CPython rejects raises its TypeError when it runs, after its arguments are evaluated.
|
staticprotected |
`arange(n)` is `arange(0, n)`: a lone start given by position is the stop.
|
protected |
Rewrite a NumPy constructor call to its canonical form in place. Returns the call lowered to a raising expression when its arguments do not bind, and None otherwise.
|
protected |
|
protected |
|
staticprotected |
|
protected |
|
staticprotected |
Whether start or stop reads a name the unpacking rebinds: the step, computed after the array, would read the rebound name.
|
protected |
Remember the names a module binds to numpy and its constructors.
|
protected |
The bound arguments of a `retstep=True` call whose step can be computed here: constant num and endpoint, start and stop safe to read twice. None otherwise.
|
protected |
|
protected |
`a, s = np.linspace(..., retstep=True)` as `a = np.linspace(...)` followed by `s = step`, the step NumPy returns: (stop - start) / div, or NaN when div, num - 1 with the endpoint and num without it, is not positive. Only for arguments that are safe to read twice.
|
protected |
The linspace call of `a, s = np.linspace(...)`, or None.
|
staticprotected |
|
staticprotected |