|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| _self_stores (fn) | |
| _init (cls) | |
| _calls_an_init (fn) | |
| _ancestors (cls, classes) | |
| _missing_attributes (cls, classes, outside_stores) | |
| _attribute_uses (module, classes) | |
| refuse_skipped_base_init (module, module_name) | |
Variables | |
| bases | |
| body | |
Refuse a read of an attribute only a skipped base `__init__` sets (#8844). When a class defines `__init__` without calling its base's, an attribute that only the base `__init__` sets is missing on its instances, and reading it raises AttributeError. The converter lays out one struct per class with every inherited attribute, so the read gets a value instead. Such a program is refused at the class's instantiation when the attribute is read anywhere.
|
protected |
The module's classes `cls` derives from, or None when one is defined elsewhere.
|
protected |
Attributes stored outside every class's `__init__`, and attributes read.
|
protected |
|
protected |
|
protected |
Attributes only a base `__init__` that `cls` skips would set.
|
protected |
Attributes `fn` stores through its first parameter.
| preprocessor.skipped_base_init.refuse_skipped_base_init | ( | module, | |
| module_name ) |
Raise NotImplementedError at the instantiation of such a class.
| preprocessor.skipped_base_init.bases |
| preprocessor.skipped_base_init.body |