chc.invariants.CNonRelationalValue module

Base class and subclasses

`chc.invariants.CNonRelationalValue.CNonRelationalValue`(...)	Base class for all non-relational values.
`chc.invariants.CNonRelationalValue.CNRVSymbolicExpr`(...)	Symbolic expression (consisting of symbolic constants).
`chc.invariants.CNonRelationalValue.CNRVSymbolicBound`(...)	Bound expressed by symbolic values.
`chc.invariants.CNonRelationalValue.CNRVIntervalValue`(...)	Numerical interval value.
`chc.invariants.CNonRelationalValue.CNRVBaseOffsetValue`(...)	Symbolic base with numerical offset (interval) value.
`chc.invariants.CNonRelationalValue.CNRVRegionSet`(...)	Set of symbolic memory regions.
`chc.invariants.CNonRelationalValue.CNRVInitializedSet`(...)	Set of initialized variables.
`chc.invariants.CNonRelationalValue.CNRVPolicyStateSet`(...)	State machine (currently not used).

Different types of non-relational values used in invariants.

class chc.invariants.CNonRelationalValue.CNRVBaseOffsetValue(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

Symbolic base with numerical offset (interval) value.

property addresstype: str

property canbenull: bool

has_lowerbound() → bool[source]

has_offsetvalue() → bool[source]

has_upperbound() → bool[source]

property is_base_offset_value: bool

property lowerbound: Optional[CXNumerical]

property offsetvalue: CXNumerical

property upperbound: Optional[CXNumerical]

property xpr: CXXpr

class chc.invariants.CNonRelationalValue.CNRVInitializedSet(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

Set of initialized variables.

property is_initialized_set: bool

property symbols: List[CXSymbol]

class chc.invariants.CNonRelationalValue.CNRVIntervalValue(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

Numerical interval value.

has_lowerbound() → bool[source]

has_upperbound() → bool[source]

has_value() → bool[source]

property is_interval_value: bool

property lowerbound: Optional[CXNumerical]

property upperbound: Optional[CXNumerical]

property value: CXNumerical

class chc.invariants.CNonRelationalValue.CNRVPolicyStateSet(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

State machine (currently not used).

property is_policy_state_set: bool

property symbols: List[CXSymbol]

class chc.invariants.CNonRelationalValue.CNRVRegionSet(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

Set of symbolic memory regions.

property is_region_set: bool

property regions: List[CXSymbol]

property size: int

class chc.invariants.CNonRelationalValue.CNRVSymbolicBound(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

Bound expressed by symbolic values.

property bound: CXprListList

property boundtype: str

property is_symbolic_bound: bool

class chc.invariants.CNonRelationalValue.CNRVSymbolicExpr(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CNonRelationalValue.CNonRelationalValue

Symbolic expression (consisting of symbolic constants).

property is_symbolic_expr: bool

property xpr: CXXpr

class chc.invariants.CNonRelationalValue.CNonRelationalValue(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CFunDictionaryRecord.CFunInvDictionaryRecord

Base class for all non-relational values.

property is_base_offset_value: bool

property is_initialized_set: bool

property is_interval_value: bool

property is_policy_state_set: bool

property is_region_set: bool

property is_symbolic_bound: bool

property is_symbolic_expr: bool