chc.api.XPredicate

Base class and subclasses:

`chc.api.XPredicate.XPredicate`(ifd, ixval)	Base class of external predicate.
`chc.api.XPredicate.XAllocationBase`(ifd, ixval)	Term points to start of allocated region that can be freed.
`chc.api.XPredicate.XBlockWrite`(ifd, ixval)	Unstructured write of bytes to pointed address with given length.
`chc.api.XPredicate.XBuffer`(ifd, ixval)	Term points to a buffer with at least a given number of bytes.
`chc.api.XPredicate.XRevBuffer`(ifd, ixval)	Term points to buffer with at least given number of bytes before the pointer
`chc.api.XPredicate.XControlledResource`(ifd, ...)	Term is not / must not be tainted.
`chc.api.XPredicate.XConfined`(ifd, ixval)	Pointer expression that is out of scope without leaking references.
`chc.api.XPredicate.XConstTerm`(ifd, ixval)	Pointed-to term is not modified.
`chc.api.XPredicate.XFalse`(ifd, ixval)	Property is always false.
`chc.api.XPredicate.XFormattedInput`(ifd, ixval)	Term is a format string.
`chc.api.XPredicate.XFreed`(ifd, ixval)	Term pointed to is freed.
`chc.api.XPredicate.XFunctional`(ifd, ixval)	Function has no observable side-effects.
`chc.api.XPredicate.XInitialized`(ifd, ixval)	Lval denoted is initialized.
`chc.api.XPredicate.XInitializedRange`(ifd, ixval)	Term pointed to is initialized for the given length (in bytes).
`chc.api.XPredicate.XInputFormatString`(ifd, ixval)	Term points to scanf format string.
`chc.api.XPredicate.XInvalidated`(ifd, ixval)	Term pointed to may not be valid any more.
`chc.api.XPredicate.XNewMemory`(ifd, ixval)	Term points to newly allocated memory (stack or heap).
`chc.api.XPredicate.XGlobalAddress`(ifd, ixval)	Term points to global memory.
`chc.api.XPredicate.XHeapAddress`(ifd, ixval)	Term points to heap memory.
`chc.api.XPredicate.XStackAddress`(ifd, ixval)	Term points to stack memory.
`chc.api.XPredicate.XNoOverlap`(ifd, ixval)	The two pointed-to memory regions do not overlap.
`chc.api.XPredicate.XNotNull`(ifd, ixval)	Term is not null.
`chc.api.XPredicate.XNonNegative`(ifd, ixval)	Term is non-negative.
`chc.api.XPredicate.XNotZero`(ifd, ixval)	Term is not zero.
`chc.api.XPredicate.XNull`(ifd, ixval)	Term is null.
`chc.api.XPredicate.XNullTerminated`(ifd, ixval)	Term is null-terminated.
`chc.api.XPredicate.XOutputFormatString`(ifd, ...)	Term points to printf-style format string.
`chc.api.XPredicate.XPreservesAllMemory`(ifd, ...)	Function does not free any external memory.
`chc.api.XPredicate.XPreservesAllMemoryX`(ifd, ...)	Function does not free any external memory except for given terms.
`chc.api.XPredicate.XPreservesMemory`(ifd, ixval)	Function does not free pointed-to memory.
`chc.api.XPredicate.XPreservesNullTermination`(...)	Function does not strip null-terminating byte from string pointed-to
`chc.api.XPredicate.XPreservesValidity`(ifd, ixval)	Validity of pointed-to resources is maintained.
`chc.api.XPredicate.XPreservesValue`(ifd, ixval)	Function does not modify the value of the term.
`chc.api.XPredicate.XRelationalExpr`(ifd, ixval)	Relational expression of terms.
`chc.api.XPredicate.XRepositioned`(ifd, ixval)	Term pointed to may be freed and reassigned.
`chc.api.XPredicate.XTainted`(ifd, ixval)	Value of term is externally controlled with optional upper/lower bound.
`chc.api.XPredicate.XUniquePointer`(ifd, ixval)	Term is the only pointer pointing at resource.
`chc.api.XPredicate.XValidMem`(ifd, ixval)	Pointed-to memory has not been freed (at time of delivery).

Object representation of sum type xpredicate_t.

Object representation of the corresponding OCaml sumtype: xpredicate_t: a predicate over s_term_t terms (terms that are visible outside of a function).

The properties of an xpredicate are constructed from its indexed value in the InterfaceDictionary

class chc.api.XPredicate.XAllocationBase(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to start of allocated region that can be freed.

args[0]: index of term in interface dictionary

property is_allocation_base: bool

property term: STerm

class chc.api.XPredicate.XBlockWrite(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Unstructured write of bytes to pointed address with given length.

args[0]: index of address term in interface dictionary
args[1]: index of length term in interface dictionary

property is_block_write: bool

property length: STerm

property term: STerm

class chc.api.XPredicate.XBuffer(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to a buffer with at least a given number of bytes.

args[0]: index of pointer to buffer in interface dictionary
args[1]: index of size term in interface dictionary

property buffer: STerm

property is_buffer: bool

property length: STerm

class chc.api.XPredicate.XConfined(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Pointer expression that is out of scope without leaking references.

args[0]: index of pointer term in interface dictionary

property is_confined: bool

property term: STerm

class chc.api.XPredicate.XConstTerm(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Pointed-to term is not modified.

args[0]: index of pointed-to term in interface dictionary

property is_const_term: bool

property term: STerm

class chc.api.XPredicate.XControlledResource(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is not / must not be tainted.

tags[1]: name of resource
args[0]: index of term in interface dictionary

property is_controlled_resource: bool

property resource: str

property size: STerm

class chc.api.XPredicate.XFalse(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Property is always false.

property is_false: bool

write_mathml(node: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XFormattedInput(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is a format string.

args[0]: index of term in interface dictionary

property is_formatted_input: bool

property term: STerm

class chc.api.XPredicate.XFreed(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term pointed to is freed.

args[0]: index of term in interface dictionary.

property is_freed: bool

property term: STerm

class chc.api.XPredicate.XFunctional(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Function has no observable side-effects.

property is_functional: bool

class chc.api.XPredicate.XGlobalAddress(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to global memory.

args[0]: index of term in interface dictionary

property is_global_address: bool

property term: STerm

class chc.api.XPredicate.XHeapAddress(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to heap memory.

args[0]: index of term in interface dictionary

property is_heap_address: bool

property term: STerm

class chc.api.XPredicate.XInitialized(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Lval denoted is initialized.

args[0]: index of lval term in interface dictionary

property is_initialized: bool

property term: STerm

write_mathml(node: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XInitializedRange(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term pointed to is initialized for the given length (in bytes).

args[0]: index of buffer pointed-to term in interface dictionary
args[1]: index of length term in interface dictionary

property buffer: STerm

property is_initialized_range: bool

property length: STerm

class chc.api.XPredicate.XInputFormatString(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to scanf format string.

args[0]: index of format-string term in interface dictionary.

property is_input_formatstring: bool

property term: STerm

class chc.api.XPredicate.XInvalidated(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term pointed to may not be valid any more.

args[0]: index of pointed-to term in interface dictionary

property is_invalidated: bool

property term: STerm

class chc.api.XPredicate.XNewMemory(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to newly allocated memory (stack or heap).

Specifically, memory that is newly allocated since the start of the function.

args[0]: index of term pointing to new memory in interface dictionary

property is_new_memory: bool

property term: STerm

class chc.api.XPredicate.XNoOverlap(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

The two pointed-to memory regions do not overlap.

args[0]: index of first term in interface dictionary args[1]: index of second term in interface dictionary

property is_no_overlap: bool

property term1: STerm

property term2: STerm

class chc.api.XPredicate.XNonNegative(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is non-negative.

args[0]: index of term in interface dictionary

property is_non_negative: bool

property term: STerm

write_mathml(cnode: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XNotNull(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is not null.

args[0]: index of term in interface dictionary

property is_not_null: bool

property term: STerm

write_mathml(cnode: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XNotZero(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is not zero.

args[0]: index of term in interface dictionary

property is_not_zero: bool

property term: STerm

write_mathml(cnode: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XNull(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is null.

args[0]: index of term in interface dictionary

property is_null: bool

property term: STerm

class chc.api.XPredicate.XNullTerminated(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is null-terminated.

args[0]: index of interface dictionary

property is_null_terminated: bool

property term: STerm

class chc.api.XPredicate.XOutputFormatString(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to printf-style format string.

args[0]: index of term in interface dictionary

property is_output_formatstring: bool

property term: STerm

class chc.api.XPredicate.XPredicate(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.InterfaceDictionaryRecord.InterfaceDictionaryRecord

Base class of external predicate.

get_iterm(argix: int) → STerm[source]

property is_allocation_base: bool

property is_block_write: bool

property is_buffer: bool

property is_confined: bool

property is_const_term: bool

property is_controlled_resource: bool

property is_false: bool

property is_formatted_input: bool

property is_freed: bool

property is_functional: bool

property is_global_address: bool

property is_heap_address: bool

property is_initialized: bool

property is_initialized_range: bool

property is_input_formatstring: bool

property is_invalidated: bool

property is_new_memory: bool

property is_no_overlap: bool

property is_non_negative: bool

property is_not_null: bool

property is_not_zero: bool

property is_null: bool

property is_null_terminated: bool

property is_output_formatstring: bool

property is_preserves_all_memory: bool

property is_preserves_all_memory_x: bool

property is_preserves_memory: bool

property is_preserves_null_termination: bool

property is_preserves_validity: bool

property is_preserves_value: bool

property is_relational_expr: bool

property is_repositioned: bool

property is_rev_buffer: bool

property is_stack_address: bool

property is_tainted: bool

property is_unique_pointer: bool

property is_valid_mem: bool

pretty() → str[source]

write_mathml(cnode: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XPreservesAllMemory(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Function does not free any external memory.

property is_preserves_all_memory: bool

class chc.api.XPredicate.XPreservesAllMemoryX(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Function does not free any external memory except for given terms.

args[0..]: indices of terms in interface dictionary

property is_preserves_all_memory_x: bool

property terms: List[STerm]

class chc.api.XPredicate.XPreservesMemory(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Function does not free pointed-to memory.

args[0]: index of term in interface dictionary

property is_preserves_memory: bool

property term: STerm

class chc.api.XPredicate.XPreservesNullTermination(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Function does not strip null-terminating byte from string pointed-to

args[0]: index of term in interface dictionary

property is_preserves_null_termination: bool

property term: STerm

class chc.api.XPredicate.XPreservesValidity(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Validity of pointed-to resources is maintained.

args[0]: index of term in interface dictionary

property is_preserves_validity: bool

property term: STerm

class chc.api.XPredicate.XPreservesValue(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Function does not modify the value of the term.

args[0]: index of term in interface dictionary

property is_preserves_value: bool

property term: STerm

class chc.api.XPredicate.XRelationalExpr(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Relational expression of terms.

tags[1]: operator
args[0]: index of first term in interface dictionary
args[1]: index of second term in interface dictionary

property is_relational_expr: bool

property op: str

pretty() → str[source]

property term1: STerm

property term2: STerm

write_mathml(cnode: xml.etree.ElementTree.Element, signature: List[str]) → None[source]

class chc.api.XPredicate.XRepositioned(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term pointed to may be freed and reassigned.

args[0]: index of term in interface dictionary

property is_repositioned: bool

property term: STerm

class chc.api.XPredicate.XRevBuffer(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to buffer with at least given number of bytes before the pointer

args[0]: index of buffer-term in interface dictionary args[1]: index of length term in interface dictionary

property buffer: STerm

property is_rev_buffer: bool

property length: STerm

class chc.api.XPredicate.XStackAddress(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term points to stack memory.

args[0]: index of term in interface dictionary

property is_stack_address: bool

property term: STerm

class chc.api.XPredicate.XTainted(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Value of term is externally controlled with optional upper/lower bound.

args[0]: index of term in interface dictionary
args[1]: index of lower bound in interface dictionary (optional)
args[2]: index of upper bound in interface dictionary (optional)

property is_tainted: bool

property lower_bound: Optional[STerm]

property term: STerm

property upper_bound: Optional[STerm]

class chc.api.XPredicate.XUniquePointer(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Term is the only pointer pointing at resource.

args[0]: index of term in interface dictionary

property is_unique_pointer: bool

property term: STerm

class chc.api.XPredicate.XValidMem(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.XPredicate.XPredicate

Pointed-to memory has not been freed (at time of delivery).

args[0]: index of term in interface dictionary

property is_valid_mem: bool

property term: STerm

chc.api.XPredicate.get_printop(s: str) → str[source]