ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
preprocessor.skipped_base_init Namespace Reference

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

Detailed Description

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.

Function Documentation

◆ _ancestors()

preprocessor.skipped_base_init._ancestors ( cls,
classes )
protected
The module's classes `cls` derives from, or None when one is defined
elsewhere.

◆ _attribute_uses()

preprocessor.skipped_base_init._attribute_uses ( module,
classes )
protected
Attributes stored outside every class's `__init__`, and attributes read.

◆ _calls_an_init()

preprocessor.skipped_base_init._calls_an_init ( fn)
protected

◆ _init()

preprocessor.skipped_base_init._init ( cls)
protected

◆ _missing_attributes()

preprocessor.skipped_base_init._missing_attributes ( cls,
classes,
outside_stores )
protected
Attributes only a base `__init__` that `cls` skips would set.

◆ _self_stores()

preprocessor.skipped_base_init._self_stores ( fn)
protected
Attributes `fn` stores through its first parameter.

◆ refuse_skipped_base_init()

preprocessor.skipped_base_init.refuse_skipped_base_init ( module,
module_name )
Raise NotImplementedError at the instantiation of such a class.

Variable Documentation

◆ bases

preprocessor.skipped_base_init.bases

◆ body

preprocessor.skipped_base_init.body