chc.invariants.CVConstantValueVariable module

Base class and subclasses

`chc.invariants.CVConstantValueVariable.CVConstantValueVariable`(vd, ...)
`chc.invariants.CVConstantValueVariable.CVVByteSequence`(vd, ...)
`chc.invariants.CVConstantValueVariable.CVVExpFunctionReturnValue`(vd, ...)	Return value from an indirect function call at a particular callsite.
`chc.invariants.CVConstantValueVariable.CVVExpSideEffectValue`(vd, ...)	Side effect value of an indirect call at a particular call site.
`chc.invariants.CVConstantValueVariable.CVVFunctionReturnValue`(vd, ...)	Return value from a direct function call at a particular callsite.
`chc.invariants.CVConstantValueVariable.CVVInitialValue`(vd, ...)	Inital value of a variable at function entry.
`chc.invariants.CVConstantValueVariable.CVVMemoryAddress`(vd, ...)	Memory address.
`chc.invariants.CVConstantValueVariable.CVVSideEffectValue`(vd, ...)	Side effect value of a direct call at a particular call site.
`chc.invariants.CVConstantValueVariable.CVVSymbolicValue`(vd, ...)	Value representing a constant-value expression.
`chc.invariants.CVConstantValueVariable.CVVTaintedValue`(vd, ...)	External input value, optionally bounded.

Symbolic values that are constant in the context of a function.

class chc.invariants.CVConstantValueVariable.CVConstantValueVariable(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CFunDictionaryRecord.CFunVarDictionaryRecord

property is_exp_function_return_value: bool

property is_exp_sideeffect_value: bool

property is_function_return_value: bool

property is_initial_value: bool

property is_memory_address: bool

property is_sideeffect_value: bool

property is_symbolic_value: bool

property is_tainted_value: bool

class chc.invariants.CVConstantValueVariable.CVVByteSequence(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

has_length() → bool[source]

property is_byte_sequence: bool

property length: CXXpr

property origin: CXVariable

class chc.invariants.CVConstantValueVariable.CVVExpFunctionReturnValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Return value from an indirect function call at a particular callsite.

args[0]: index of callsite location in file declarations
args[1]: index of porgramcontext in context dictionary
args[2]: index of indirect call expression in xprdictionary
args[3]: index of the typ of the call expression in the cdictionary
args[4..]: indices of argument expressions to the call in the xprdictionary

property arguments: List[Optional[CXXpr]]

property callee: CXXpr

property is_exp_function_return_value: bool

property location: CLocation

class chc.invariants.CVConstantValueVariable.CVVExpSideEffectValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Side effect value of an indirect call at a particular call site.

args[0]: index of callsite location in file declarations
args[1]: index of programcontext in context dictionary
args[2]: index of the indirect call expression in the xprdictionary
args[3]: argument index of the side-effect value (starting at 1)
args[4]: index of the type of the side-effect value in cdictionary
args[5..]: indices of the arguments passed to the call in xprdictionary

property argindex: int

property arguments: List[Optional[CXXpr]]

property callee: CXXpr

property is_exp_side_effect_value: bool

property location: CLocation

property typ: CTyp

class chc.invariants.CVConstantValueVariable.CVVFunctionReturnValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Return value from a direct function call at a particular callsite.

args[0]: index of callsite location in file declarations
args[1]: index of programcontext in context dictionary
args[2]: vid of the varinfo of the function called
args[3..]: indices of argument expressions to the call in the xprdictionary

property arguments: List[Optional[CXXpr]]

property callee: CVarInfo

property is_function_return_value: bool

property location: CLocation

class chc.invariants.CVConstantValueVariable.CVVInitialValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Inital value of a variable at function entry.

args[0]: index of original variable in the xprdictionary
args[1]: index of variable type in cdictionary

property is_initial_value: bool

property typ: CTyp

property variable: CXVariable

class chc.invariants.CVConstantValueVariable.CVVMemoryAddress(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Memory address.

args[0]: memory reference index
args[1]: index of the offset in the cdictionary

property is_memory_address: bool

property memory_reference: CVMemoryReferenceData

property offset: COffset

class chc.invariants.CVConstantValueVariable.CVVSideEffectValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Side effect value of a direct call at a particular call site.

args[0]: index of callsite location in file declarations
args[1]: index of programcontext in context dictionary
args[2]: vid of the varinfo of the function called
args[3]: argument index of the side-effect (index starting at 1)
args[4]: index of the type of side-effect value in cdictionary
args[5..]: indices of the arguments passed to the call in xprdictionary

property argindex: int

property arguments: List[Optional[CXXpr]]

property callee: CVarInfo

property is_side_effect_value: bool

property location: CLocation

property typ: CTyp

class chc.invariants.CVConstantValueVariable.CVVSymbolicValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

Value representing a constant-value expression.

args[0]: index of the original expression in the xprdictionary
args[1]: index of the type of the expression in the cdictionary

property is_symbolic_value: bool

property typ: CTyp

property xpr: CXXpr

class chc.invariants.CVConstantValueVariable.CVVTaintedValue(vd: CFunVarDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.invariants.CVConstantValueVariable.CVConstantValueVariable

External input value, optionally bounded.

args[0]: index of the external variable in the xprdictionary
args[1]: index of lower bound value in xprdictionary (or -1 for unbounded)
args[2]: index of upper bound vlaue in xprdictionary (or -1 for unbounded)
args[3]: index of the type of the variable in the cdictionary

has_lowerbound() → bool[source]

has_upperbound() → bool[source]

property is_tainted_value: bool

property lowerbound: CXXpr

property origin: CXVariable

property typ: CTyp

property upperbound: CXXpr