|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <nlohmann/json.hpp>#include <util/irep/expr.h>#include <optional>#include <string>#include <tuple>#include <vector>Go to the source code of this file.
Classes | |
| struct | numpy_nditer_operand |
| One operand of an nditer: a named array or view and its layout in elements (a negative stride walks backwards, 0 repeats a broadcast axis). More... | |
| struct | numpy_nditer_state |
| The static description of an np.nditer: its operands, the iteration shape, and the order the positions are visited in. More... | |
| struct | numpy_nditer_item |
| A name bound to what an nditer yields: the element (or the external-loop chunk) of one operand at the position captured when it was bound. More... | |
| class | numpy_nditer |
| np.nditer as an iterator object over named arrays and views (ADR-NP-003): the converter keeps its position in hidden variables and lowers every read through the operand's own subscript, in the order NumPy visits it (C, F, or K: memory order, negative strides undone). More... | |