|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| is_dataclass (self, class_node) | |
| collect_fields (self, class_node) | |
| build_init (self, class_node, fields) | |
| build_dataclass_repr (self, class_node, fields) | |
| build_dataclass_eq (self, class_node, fields) | |
| build_dataclass_hash (self, class_node, fields) | |
| build_dataclass_order (self, class_node, fields, method_name, op_cls) | |
| build_dataclass_fields_metadata (self, class_node, fields) | |
| expand_dataclass (self, class_node) | |
Public Attributes | |
| dataclasses_module_names | |
| known_variable_types | |
| instance_class_map | |
| typing_module_names | |
| class_attr_annotations | |
Protected Member Functions | |
| _ensure_dataclass_initvar_import (self, module_node) | |
| _build_dataclass_field_helper_class (self, source_node) | |
| _build_dataclass_replace_error_helper (self, source_node) | |
| _build_dataclass_getattr_helper (self, source_node) | |
| _dataclass_api_kind_from_name (self, name) | |
| _dataclass_api_kind (self, node) | |
| _dataclass_instance_type_of_expr (self, expr) | |
| _dataclass_class_of_expr (self, expr) | |
| _annotation_class_name (self, annotation) | |
| _dataclass_field_specs (self, class_name) | |
| _build_recursive_dataclass_call (self, walk_name, value_expr, source_node) | |
| _build_static_known_dataclass_expr (self, kind, class_name, instance_expr, source_node) | |
| _walk_recurse_on_item (self, source_node) | |
| _build_walk_dict_comp (self, source_node) | |
| _build_walk_iter_call (self, builder, source_node) | |
| _build_walk_dataclass_expr (self, kind, source_node) | |
| _build_runtime_recursive_dataclass_expr (self, kind, instance_expr, source_node) | |
| _build_asdict_expr (self, class_name, instance_expr, source_node) | |
| _build_astuple_expr (self, class_name, instance_expr, source_node) | |
| _rewrite_dataclass_replace_call (self, instance_class, target, node) | |
| _rewrite_dataclass_fields_call (self, node, effective_class) | |
| _rewrite_is_dataclass_call (self, node, target, class_name, instance_class) | |
| _rewrite_dataclass_fields_kind (self, node, class_name, instance_class) | |
| _rewrite_dataclass_instance_kind (self, kind, node, target, instance_class) | |
| _rewrite_dataclass_api_call (self, node) | |
| _unwrap_annotation_slice (self, annotation) | |
| _is_dataclass_initvar_base (self, node) | |
| _is_typing_classvar_base (self, node) | |
| _analyze_dataclass_field_annotation (self, annotation) | |
| _get_post_init_method (self, class_node) | |
| _class_has_post_init_behavior (self, class_node) | |
| _class_defines_name (self, class_node, name) | |
| _validate_post_init_signature (self, class_node, fields, post_init_method) | |
| _dataclass_default_options (self) | |
| _field_spec (self, name, annotation, defaults, options) | |
| _parse_dataclass_bool_option (self, value, option_name) | |
| _parse_dataclass_options (self, class_node) | |
| _is_field_call (self, call_node) | |
| _parse_field_hash_value (self, value) | |
| _apply_field_keyword (self, kw, state) | |
| _parse_field_call (self, default_value) | |
| _build_init_args (self, class_node, fields) | |
| _build_init_field_rhs (self, class_node, field) | |
| _build_init_field_assigns (self, class_node, fields) | |
| _build_post_init_call_stmt (self, class_node, initvar_names) | |
| _build_tuple_from_fields (self, class_node, fields, predicate) | |
| _record_dataclass_attr_annotations (self, class_node, fields) | |
| _inject_dataclass_synth_methods (self, class_node, fields, dataclass_options, insert_index) | |
Static Protected Member Functions | |
| _walk_isinstance_ifexp (type_name, body, orelse) | |
| _walker_two_arg_args () | |
| _partition_init_fields (fields) | |
| _build_init_positional_defaults (pos_fields) | |
| _validate_dataclass_field_ordering (class_node, fields) | |
| _strip_field_annassigns (class_node, fields) | |
| _compute_init_insert_index (class_node) | |
| _class_defines_method (class_node, method_name) | |
Static Protected Attributes | |
| dict | _DATACLASS_API_ATTR_KINDS |
| dict | _DATACLASS_INSTANCE_HANDLERS |
| _FIELD_ALLOWED_OPTS | |
| _FIELD_BOOL_OPTS = frozenset({"init", "repr", "compare", "kw_only"}) | |
|
protected |
Classify a dataclass annotation as instance field, InitVar or ClassVar.
|
protected |
|
protected |
Mutate ``state`` with the value carried by ``kw``.
``state`` is the dict ``{"default_expr": ..., "factory_expr": ...,
"options": {...}}`` populated by ``_parse_field_call``.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
Return (args, defaults, kwonlyargs, kw_defaults, initvar_names).
|
protected |
Build ``self.<field> = ...`` assignments for instance fields. Emits plain ``Assign`` statements rather than ``AnnAssign`` for ``self.<field>``. Optional-typed instance attributes are already handled by the normal class/parameter typing paths, whereas an explicit ``self.x: Optional[T] = ...`` here can confuse later arithmetic over values proven non-None by guards (see optional7).
|
protected |
Return the RHS expression for an instance field assignment.
|
staticprotected |
Return positional ``defaults`` list mirroring trailing pos_fields.
|
protected |
Return an ``Expr`` calling ``__post_init__`` or ``None``. When the class defines ``__post_init__`` directly, the call is addressed as ``ClassName.__post_init__(self, *initvars)`` so the unbound-method form is preserved. Otherwise, if the class merely inherits a ``__post_init__`` (detected by behavior), the call uses the bound form ``self.__post_init__(*initvars)``.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
Return ``builder(elt)`` over the items of ``_VALUE``. ``builder`` must be ``ast.ListComp`` or wrap ``ast.GeneratorExp``; the generator iterates ``_VALUE`` binding ``_ITEM`` on each step.
|
staticprotected |
|
protected |
|
protected |
|
staticprotected |
Return 1 if the class body opens with a docstring, else 0.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
Return a normalized field spec. ``defaults`` is the ``(default_expr, factory_expr)`` pair returned by ``_parse_field_call``. ``options`` carries per-field flags plus ``"kind"`` (one of ``instance``, ``initvar``, ``classvar``).
|
protected |
|
protected |
Insert __init__/fields metadata/__repr__/__eq__/order/__hash__.
|
protected |
|
protected |
Return True if ``call_node`` invokes ``dataclasses.field``.
|
protected |
|
protected |
|
protected |
|
protected |
Decompose ``field(...)`` calls into (default_expr, factory_expr, options).
Returns a triple where ``default_expr`` is the AST node for the
``default=`` value (or the original raw value when ``default_value`` is
not a ``field(...)`` call), and ``factory_expr`` is the AST node passed
as ``default_factory=`` (or ``None`` when not present).
The model in ``models/dataclasses.py`` already collapses
``field(default=X)`` to ``X`` and ``field(default_factory=F)`` to
``F()`` at runtime, but operating at AST level lets us:
* keep ``default=`` literals as ordinary Python defaults
(cheap and consistent with Marco B), and
* desugar ``default_factory=`` into a per-instance call so each
constructed object gets a fresh value.
|
protected |
|
staticprotected |
Split fields into (param_fields, pos_fields, kwonly_fields, initvar_names).
|
protected |
Preserve instance-field annotations for later attribute lookups.
|
protected |
|
protected |
Rewrite ``fields(Cls or instance)`` into a literal list of fields.
|
protected |
|
protected |
|
protected |
Rewrite ``replace(obj, k=v, ...)`` into ``Cls(...)`` when possible. Returns ``node`` unchanged if a ``**kwargs`` splat prevents resolution, or an error-helper call when an unknown field is referenced.
|
protected |
|
staticprotected |
Remove ``x: T [= ...]`` declarations now subsumed by ``__init__``.
|
protected |
|
staticprotected |
Raise SyntaxError if a non-default field follows a defaulted one. Mirrors CPython's ``non-default argument follows default argument`` diagnostic. Class variables and keyword-only fields are exempt.
|
protected |
Validate that ``__post_init__`` can receive the declared InitVar values.
|
staticprotected |
|
protected |
|
staticprotected |
| preprocessor.dataclass_mixin.DataclassMixin.build_dataclass_eq | ( | self, | |
| class_node, | |||
| fields ) |
| preprocessor.dataclass_mixin.DataclassMixin.build_dataclass_fields_metadata | ( | self, | |
| class_node, | |||
| fields ) |
| preprocessor.dataclass_mixin.DataclassMixin.build_dataclass_hash | ( | self, | |
| class_node, | |||
| fields ) |
| preprocessor.dataclass_mixin.DataclassMixin.build_dataclass_order | ( | self, | |
| class_node, | |||
| fields, | |||
| method_name, | |||
| op_cls ) |
| preprocessor.dataclass_mixin.DataclassMixin.build_dataclass_repr | ( | self, | |
| class_node, | |||
| fields ) |
| preprocessor.dataclass_mixin.DataclassMixin.build_init | ( | self, | |
| class_node, | |||
| fields ) |
Build __init__(self, ...) that assigns self.<field> = <field>. Supports raw defaults (``x: int = 5``), ``field(default=...)`` and ``field(default_factory=...)``. Factory fields are exposed as ``__init__`` parameters with ``None`` as default so signature ordering and defaults match expectations from the dataclass preprocessor tests. The assignment remains a direct ``self.<field> = <factory>()`` in the body.
| preprocessor.dataclass_mixin.DataclassMixin.collect_fields | ( | self, | |
| class_node ) |
Collect dataclass field specs. Each entry is ``(name, annotation, default_expr, factory_expr, kind)`` where ``kind`` is one of ``instance``, ``initvar`` or ``classvar``.
| preprocessor.dataclass_mixin.DataclassMixin.expand_dataclass | ( | self, | |
| class_node ) |
Inject a minimal generated __init__ for dataclass-decorated classes.
| preprocessor.dataclass_mixin.DataclassMixin.is_dataclass | ( | self, | |
| class_node ) |
Return True when a class is decorated with @dataclass. Recognizes the canonical ``@dataclass`` form, the qualified ``@dataclasses.dataclass`` form, and any local alias introduced via ``from dataclasses import dataclass as <alias>`` (tracked in ``self._dataclass_decorator_names``).
|
protected |
|
staticprotected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
staticprotected |
|
protected |
|
protected |
|
staticprotected |
|
staticprotected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
| preprocessor.dataclass_mixin.DataclassMixin.class_attr_annotations |
| preprocessor.dataclass_mixin.DataclassMixin.dataclasses_module_names |
| preprocessor.dataclass_mixin.DataclassMixin.instance_class_map |
| preprocessor.dataclass_mixin.DataclassMixin.known_variable_types |
| preprocessor.dataclass_mixin.DataclassMixin.typing_module_names |