chc.proof.CPOPredicate module

Base class and subclasses:

chc.proof.CPOPredicate.CPOAllocationBase(pd, ...)

allocation-base(exp): exp is the start address of a dynamically allocated region.

chc.proof.CPOPredicate.CPOBuffer(pd, ixval)

buffer(exp, size): exp points to a buffer of at least size bytes.

chc.proof.CPOPredicate.CPOCast(pd, ixval)

cast(srctyp, tgttyp, exp): cast of exp from srctyp to tgttyp is safe.

chc.proof.CPOPredicate.CPOCommonBase(pd, ixval)

common-base(exp1, exp2): pointer expressions exp1 and exp2 point into the same object.

chc.proof.CPOPredicate.CPOCommonBaseType(pd, ...)

common-base-type(exp1, exp2): pointer expressions exp1 and exp2 point into objects with the same type.

chc.proof.CPOPredicate.CPOControlledResource(pd, ...)

controlled-resource(name, exp): controlled resource, with [name] is not tainted.

chc.proof.CPOPredicate.CPODistinctRegion(pd, ...)

Memory referenced by i is disinct from memory pointed to by exp.

chc.proof.CPOPredicate.CPOFormatCast(pd, ixval)

format-cast(srctyp, tgttyp, exp): cast of exp from srctyp to tgttyp is safe

chc.proof.CPOPredicate.CPOFormatString(pd, ixval)

format-string(exp): pointer exp points to a format string.

chc.proof.CPOPredicate.CPOGlobalAddress(pd, ...)

global-address(exp): exp is a global address

chc.proof.CPOPredicate.CPOHeapAddress(pd, ixval)

heap-address(exp): exp is a heap address

chc.proof.CPOPredicate.CPOInScope(pd, ixval)

in-scope(exp): memory pointed to by exp is in scope.

chc.proof.CPOPredicate.CPOIndexLowerBound(pd, ...)

index-lower-bound(exp): the value of index expression exp is greater than or equal to zero.

chc.proof.CPOPredicate.CPOIndexUpperBound(pd, ...)

index-upper-bound(exp): the value of index expression exp is less than the size of the array.

chc.proof.CPOPredicate.CPOInitialized(pd, ixval)

initialized(lval): location lval has been initialized.

chc.proof.CPOPredicate.CPOInitializedRange(pd, ...)

initialized-range(exp, size): the memory range starting at the address pointed to by exp is initialized for at least size bytes.

chc.proof.CPOPredicate.CPOIntOverflow(pd, ixval)

int-overflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an integer overflow

chc.proof.CPOPredicate.CPOIntUnderflow(pd, ixval)

int-underflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an integer underflow

chc.proof.CPOPredicate.CPOLowerBound(pd, ixval)

lower-bound(typ, exp): the value of pointer exp is greater than or equal to zero.

chc.proof.CPOPredicate.CPONewMemory(pd, ixval)

new-memory(exp): the memory pointed to was allocated fresh (not aliased).

chc.proof.CPOPredicate.CPONoOverlap(pd, ixval)

no-overlap(exp1, exp2): the objects pointed to by exp1 and exp2 do not overlap.

chc.proof.CPOPredicate.CPONonNegative(pd, ixval)

non-negative(exp): exp is nonnegative (>= 0)

chc.proof.CPOPredicate.CPONotNull(pd, ixval)

not-null(exp): exp is not NULL

chc.proof.CPOPredicate.CPONotZero(pd, ixval)

not-zero(exp): exp is not zero

chc.proof.CPOPredicate.CPONull(pd, ixval)

null(exp): the expression is NULL

chc.proof.CPOPredicate.CPONullTerminated(pd, ...)

null-terminated(exp): the string pointed to by exp is null-terminated

chc.proof.CPOPredicate.CPOPointerCast(pd, ixval)

pointer-cast(srctyp, tgttyp, exp): cast of exp from srctyp to tgttyp is safe

chc.proof.CPOPredicate.CPOPredicate(pd, ixval)

Base class for all predicates.

chc.proof.CPOPredicate.CPOPreservedAllMemory(pd, ...)

preserves-all-memory(): true of a function that does not free any memory.

chc.proof.CPOPredicate.CPOPreservedValue(pd, ...)

preserves-value(exp): true of a function that preserves the value of exp.

chc.proof.CPOPredicate.CPOPtrLowerBound(pd, ...)

ptr-lower-bound(exp1, exp2, op, typ): the pointer arithmetic operation exp1 op exp2 with resulttype typ does not violate its lower bound.

chc.proof.CPOPredicate.CPOPtrUpperBound(pd, ...)

ptr-upper-bound(exp1, exp2, op, typ): the pointer arithmetic operation exp1 op exp2 with resulttype typ does not violate its upper bound.

chc.proof.CPOPredicate.CPOPtrUpperBoundDeref(pd, ...)

ptr-upper-bound-deref(exp1, exp2, op, typ): the pointer arithmetic operation exp1 op exp2 with resulttype typ does not violate its upper bound.

chc.proof.CPOPredicate.CPORevBuffer(pd, ixval)

rev-buffer(exp, size) exp points into a buffer with at least size bytes preceding.

chc.proof.CPOPredicate.CPOSignedToSignedCastLB(pd, ...)

signed-to-signed-cast-lb(srckind, tgtkind, exp): integer cast from signed srckind to signed tgtkind is safe wrt its lowerbound.

chc.proof.CPOPredicate.CPOSignedToSignedCastUB(pd, ...)

signed-to-signed-cast-ub(srckind, tgtkind, exp): integer cast from signed srckind to tgtkind is safe wrt to its upperbound.

chc.proof.CPOPredicate.CPOSignedToUnsignedCastLB(pd, ...)

signed-to-unsigned-cast-lb(srckind, tgtkind, exp): integer cast of exp from signed srckind to unsigned tgtkind is safe wrt its lowerbound

chc.proof.CPOPredicate.CPOSignedToUnsignedCastUB(pd, ...)

signed-to-unsigned-cast-ub(srckind, tgtkind, exp): integer cast from signed srckind to unsigned ikind is safe wrt its upperbound

chc.proof.CPOPredicate.CPOStackAddressEscape(pd, ...)

Pointer is not assigned to lval with longer lifetime and is not returned.

chc.proof.CPOPredicate.CPOTypeAtOffset(pd, ixval)

type-at-offset(typ, exp): exp has the given type.

chc.proof.CPOPredicate.CPOUIntOverflow(pd, ixval)

uint-overflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an unsigned integer underflow

chc.proof.CPOPredicate.CPOUIntUnderflow(pd, ...)

uint-underflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an unsigned integer underflow

chc.proof.CPOPredicate.CPOUnsignedToSignedCast(pd, ...)

unsigned-to-signed cast(srckind, tgtkind, exp): integer cast from srckind to tgtkind is safe.

chc.proof.CPOPredicate.CPOUnsignedToUnsignedCast(pd, ...)

unsigned-to-unsigned-cast(srckind, tgtkind, exp): integer cast from unsigned srckind to unsigned tgtkind is safe.

chc.proof.CPOPredicate.CPOUpperBound(pd, ixval)

upper-bound(typ, exp): the value of pointer exp is less than or equal to the maximum address allowed by typ.

chc.proof.CPOPredicate.CPOValidMem(pd, ixval)

valid-mem(exp): exp points to valid memory (not freed).

chc.proof.CPOPredicate.CPOValueConstraint(pd, ...)

value-constraint(exp): boolean expression exp evaluates to true.

chc.proof.CPOPredicate.CPOVarArgs(pd, ixval)

var-args(fmt, n, args): the number or arguments provided matches the number of arguments requested by the format string.

chc.proof.CPOPredicate.CPOWidthOverflow(pd, ...)

width-overflow(exp, ikind): the value of the expression fits in an integer of ikind.

Proof obligation predicate.

class chc.proof.CPOPredicate.CPOAllocationBase(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

allocation-base(exp): exp is the start address of a dynamically allocated region.

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_allocation_base: bool
class chc.proof.CPOPredicate.CPOBuffer(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

buffer(exp, size): exp points to a buffer of at least size bytes.

  • args[0]: index of exp in cdictionary

  • args[1]: index of size in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_buffer: bool
property size: CExp
class chc.proof.CPOPredicate.CPOCast(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

cast(srctyp, tgttyp, exp): cast of exp from srctyp to tgttyp is safe.

  • args[0]: index of srctyp in cdictionary

  • args[1]: index of tgttyp in cdictionary

  • args[2]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_cast: bool
property srctyp: CTyp
property tgttyp: CTyp
class chc.proof.CPOPredicate.CPOCommonBase(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

common-base(exp1, exp2): pointer expressions exp1 and exp2 point into the same object.

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_common_base: bool
class chc.proof.CPOPredicate.CPOCommonBaseType(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

common-base-type(exp1, exp2): pointer expressions exp1 and exp2 point into objects with the same type.

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_common_base_type: bool
class chc.proof.CPOPredicate.CPOControlledResource(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

controlled-resource(name, exp): controlled resource, with [name] is not tainted.

  • tags[1]: name of resource

  • args[0]: index of exp in cdictionary

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_controlled_resource: bool
property resource: str
class chc.proof.CPOPredicate.CPODistinctRegion(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

Memory referenced by i is disinct from memory pointed to by exp.

  • args[0]: index of exp in cdictionary

  • args[1]: memref index

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_distinct_region: bool
property memref: int
class chc.proof.CPOPredicate.CPOFormatCast(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

format-cast(srctyp, tgttyp, exp): cast of exp from srctyp to tgttyp is safe

Note: this predicate is used specifically in the context of the cast of an argument passed for a given format argument specifier.

  • args[0]: index of srctyp in cdictionary

  • args[1]: index of tgttyp in tgtdictionary

  • args[2]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_format_cast: bool
property srctyp: CTyp
property tgttyp: CTyp
class chc.proof.CPOPredicate.CPOFormatString(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

format-string(exp): pointer exp points to a format string.

Note: this property reflects best practices, to ensure that functions that expect a format string argument are not invoked with a user-constructed string. This property does not directly lead to undefined behavior.

  • args[0]: index exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_format_string: bool
class chc.proof.CPOPredicate.CPOGlobalAddress(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

global-address(exp): exp is a global address

  • args[0]: index of exp in cdictionary

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_global_address: bool
class chc.proof.CPOPredicate.CPOHeapAddress(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

heap-address(exp): exp is a heap address

  • args[0]: index of exp in cdictionary

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_heap_address: bool
class chc.proof.CPOPredicate.CPOInScope(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

in-scope(exp): memory pointed to by exp is in scope.

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_in_scope: bool
class chc.proof.CPOPredicate.CPOIndexLowerBound(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

index-lower-bound(exp): the value of index expression exp is greater than or equal to zero.

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_index_lower_bound: bool
class chc.proof.CPOPredicate.CPOIndexUpperBound(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

index-upper-bound(exp): the value of index expression exp is less than the size of the array.

  • args[0]: index of exp in cdictionary

  • args[1]: index of array size expression in cdictionary

property bound: CExp
property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_index_upper_bound: bool
class chc.proof.CPOPredicate.CPOInitialized(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

initialized(lval): location lval has been initialized.

  • args[0]: index of lval in cdictionary

has_ref_type() → bool[source]
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

has_variable_deref(vid: int) → bool[source]

Return true if the with variable with vid is dereferenced in any subexpression.

property is_initialized: bool
property lval: CLval
class chc.proof.CPOPredicate.CPOInitializedRange(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

initialized-range(exp, size): the memory range starting at the address pointed to by exp is initialized for at least size bytes.

  • args[0]: index of exp in cdictionary

  • args[1]: index of size in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_initialized_range: bool
property size: CExp
class chc.proof.CPOPredicate.CPOIntOverflow(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

int-overflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an integer overflow

  • tags[1]: binop

  • tags[2]: ikind

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property ikind: str
property is_int_overflow: bool
class chc.proof.CPOPredicate.CPOIntUnderflow(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

int-underflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an integer underflow

  • tags[1]: binop

  • tags[2]: ikind

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property ikind: str
property is_int_underflow: bool
class chc.proof.CPOPredicate.CPOLowerBound(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

lower-bound(typ, exp): the value of pointer exp is greater than or equal to zero.

  • args[0]: index of typ in cdictionary

  • args[1]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_lower_bound: bool
property typ: CTyp
class chc.proof.CPOPredicate.CPONewMemory(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

new-memory(exp): the memory pointed to was allocated fresh (not aliased).

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_new_memory: bool
class chc.proof.CPOPredicate.CPONoOverlap(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

no-overlap(exp1, exp2): the objects pointed to by exp1 and exp2 do not overlap.

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_no_overlap: bool
class chc.proof.CPOPredicate.CPONonNegative(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

non-negative(exp): exp is nonnegative (>= 0)

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_non_negative: bool
class chc.proof.CPOPredicate.CPONotNull(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

not-null(exp): exp is not NULL

args[0]: index of exp in cdictionary

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_not_null: bool
class chc.proof.CPOPredicate.CPONotZero(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

not-zero(exp): exp is not zero

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_not_zero: bool
class chc.proof.CPOPredicate.CPONull(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

null(exp): the expression is NULL

  • args[0]: exp

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_null: bool
class chc.proof.CPOPredicate.CPONullTerminated(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

null-terminated(exp): the string pointed to by exp is null-terminated

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_null_terminated: bool
class chc.proof.CPOPredicate.CPOPointerCast(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

pointer-cast(srctyp, tgttyp, exp): cast of exp from srctyp to tgttyp is safe

Note: this predicate is used specifically for casting of pointers to other pointers

  • args[0]: index of srctyp in cdictionary

  • args[1]: index of tgttyp in tgtdictionary

  • args[2]: index of exp in cdictionary

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_pointer_cast: bool
property srctyp: CTyp
property tgttyp: CTyp
class chc.proof.CPOPredicate.CPOPredicate(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CFilePredicateRecord.CFilePredicateRecord

Base class for all predicates.

has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_ref_type() → bool[source]
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

has_variable_deref(vid: int) → bool[source]

Return true if the with variable with vid is dereferenced in any subexpression.

has_variable_op(vid: int, op: str) → bool[source]
property is_allocation_base: bool
property is_buffer: bool
property is_can_leave_scope: bool
property is_cast: bool
property is_common_base: bool
property is_controlled_resource: bool
property is_format_cast: bool
property is_format_string: bool
property is_global_address: bool
property is_heap_address: bool
property is_in_scope: bool
property is_index_lower_bound: bool
property is_index_upper_bound: bool
property is_initialized: bool
property is_initialized_range: bool
property is_int_overflow: bool
property is_int_underflow: bool
property is_lower_bound: 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_pointer_cast: bool
property is_preserved_all_memory: bool
property is_ptr_lower_bound: bool
property is_ptr_upper_bound: bool
property is_ptr_upper_bound_deref: bool
property is_rev_buffer: bool
property is_signed_to_signed_cast_lb: bool
property is_signed_to_signed_cast_ub: bool
property is_signed_to_unsigned_cast_lb: bool
property is_signed_to_unsigned_cast_ub: bool
property is_stack_address_escape: bool
property is_type_at_offset: bool
property is_unsigned_to_signed_cast: bool
property is_unsigned_to_unsigned_cast: bool
property is_upper_bound: bool
property is_valid_mem: bool
property is_value_constraint: bool
property is_width_overflow: bool
property predicate_name: str
tgtkind() → str[source]
class chc.proof.CPOPredicate.CPOPreservedAllMemory(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

preserves-all-memory(): true of a function that does not free any memory.

property is_preserves_all_memory: bool
class chc.proof.CPOPredicate.CPOPreservedValue(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

preserves-value(exp): true of a function that preserves the value of exp.

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

class chc.proof.CPOPredicate.CPOPtrLowerBound(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

ptr-lower-bound(exp1, exp2, op, typ): the pointer arithmetic operation exp1 op exp2 with resulttype typ does not violate its lower bound.

  • tags[1]: binop

  • args[0]: typ

  • args[1]: exp1

  • args[2]: exp2

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_ptr_lower_bound: bool
property typ: CTyp
class chc.proof.CPOPredicate.CPOPtrUpperBound(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

ptr-upper-bound(exp1, exp2, op, typ): the pointer arithmetic operation exp1 op exp2 with resulttype typ does not violate its upper bound.

  • tags[1]: binop

  • args[0]: typ

  • args[1]: exp1

  • args[2]: exp2

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_ptr_upper_bound: bool
property typ: CTyp
class chc.proof.CPOPredicate.CPOPtrUpperBoundDeref(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

ptr-upper-bound-deref(exp1, exp2, op, typ): the pointer arithmetic operation exp1 op exp2 with resulttype typ does not violate its upper bound.

  • tags[1]: binop

  • args[0]: typ

  • args[1]: exp1

  • args[2]: exp2

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_ptr_upper_bound_deref: bool
property typ: CTyp
class chc.proof.CPOPredicate.CPORevBuffer(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

rev-buffer(exp, size) exp points into a buffer with at least size bytes preceding.

  • args[0]: index of exp in cdictionary

  • args[1]: index of presize expression in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_rev_buffer: bool
property size: CExp
class chc.proof.CPOPredicate.CPOSignedToSignedCastLB(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

signed-to-signed-cast-lb(srckind, tgtkind, exp): integer cast from signed srckind to signed tgtkind is safe wrt its lowerbound.

  • tags[1]: srckind

  • tags[2]: tgtkind

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_signed_to_signed_cast_lb: bool
property srckind: str
property tgtkind: str
class chc.proof.CPOPredicate.CPOSignedToSignedCastUB(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

signed-to-signed-cast-ub(srckind, tgtkind, exp): integer cast from signed srckind to tgtkind is safe wrt to its upperbound.

  • tags[1]: srckind

  • tags[2]: tgtkind

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_signed_to_signed_cast_ub: bool
property srckind: str
property tgtkind: str
class chc.proof.CPOPredicate.CPOSignedToUnsignedCastLB(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

signed-to-unsigned-cast-lb(srckind, tgtkind, exp): integer cast of exp from signed srckind to unsigned tgtkind is safe wrt its lowerbound

  • tags[1]: srckind

  • tags[2]: tgtkind

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_signed_to_unsigned_cast_lb: bool
property srckind: str
property tgtkind: str
class chc.proof.CPOPredicate.CPOSignedToUnsignedCastUB(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

signed-to-unsigned-cast-ub(srckind, tgtkind, exp): integer cast from signed srckind to unsigned ikind is safe wrt its upperbound

  • tags[1]: srckind

  • tags[2]: tgtkind

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_signed_to_unsigned_cast_ub: bool
property srckind: str
property tgtkind: str
class chc.proof.CPOPredicate.CPOStackAddressEscape(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

Pointer is not assigned to lval with longer lifetime and is not returned.

  • args[0]: index of lval in cdictionary or -1 if None

  • args[1]: index exp in cdictionary

property exp: CExp
has_lval() → bool[source]
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_stack_address_escape: bool
property lval: CLval
class chc.proof.CPOPredicate.CPOTypeAtOffset(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

type-at-offset(typ, exp): exp has the given type.

  • args[0]: index of typ in cdictionary

  • args[1]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_type_at_offset: bool
property typ: CTyp
class chc.proof.CPOPredicate.CPOUIntOverflow(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

uint-overflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an unsigned integer underflow

Note: this property is kept separate, because it does not lead to undefined behavior and can be enabled/disabled as desired.

  • tags[1]: binop

  • tags[2]: ikind

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property ikind: str
property is_uint_overflow: bool
class chc.proof.CPOPredicate.CPOUIntUnderflow(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

uint-underflow(exp1, exp2, binop): the result of the binary operation exp1 binop exp2 does not result in an unsigned integer underflow

Note: this property is kept separate, because it does not lead to undefined behavior and can be enabled/disabled as desired.

  • tags[1]: binop

  • tags[2]: ikind

  • args[0]: index of exp1 in cdictionary

  • args[1]: index of exp2 in cdictionary

property binop: str
property exp1: CExp
property exp2: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property ikind: str
property is_uint_underflow: bool
class chc.proof.CPOPredicate.CPOUnsignedToSignedCast(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

unsigned-to-signed cast(srckind, tgtkind, exp): integer cast from srckind to tgtkind is safe.

  • tags[1]: srckind

  • tags[2]: tgtkind

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_unsigned_to_signed_cast: bool
property srckind: str
property tgtkind: str
class chc.proof.CPOPredicate.CPOUnsignedToUnsignedCast(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

unsigned-to-unsigned-cast(srckind, tgtkind, exp): integer cast from unsigned srckind to unsigned tgtkind is safe.

  • tags[1]: srckind

  • tags[2]: tgtkind

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_unsigned_to_unsigned_cast: bool
property srckind: str
property tgtkind: str
class chc.proof.CPOPredicate.CPOUpperBound(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

upper-bound(typ, exp): the value of pointer exp is less than or equal to the maximum address allowed by typ.

  • args[0]: index of typ in cdictionary

  • args[1]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_upper_bound: bool
property typ: CTyp
class chc.proof.CPOPredicate.CPOValidMem(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

valid-mem(exp): exp points to valid memory (not freed).

  • args[0]: index of exp in cdictionary

property exp: CExp
has_argument(vid: int) → bool[source]

Return true if the single exp predicate argument is the variable with vid.

has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_valid_mem: bool
class chc.proof.CPOPredicate.CPOValueConstraint(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

value-constraint(exp): boolean expression exp evaluates to true.

Note: although most properties could be expressed as value constraints, it is preferable to use the dedicated property if available, to better convey the origin of the proof obligation (and possibly add additional context information)

  • args[0]: index of exp in cdictionary

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property is_value_constraint: bool
class chc.proof.CPOPredicate.CPOVarArgs(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

var-args(fmt, n, args): the number or arguments provided matches the number of arguments requested by the format string.

  • args[0]: index of fmt (pointer to format string) in cdictionary

  • args[1]: expected number of arguments

  • args[2]: args:

    • 0: int (expected number of arguments)

    • 1: index of fmt in cdictionary

    • 2..: indices of args in cdictionary

property argcount: int
property arguments: List[CExp]
property fmt: CExp
class chc.proof.CPOPredicate.CPOWidthOverflow(pd: CFilePredicateDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CPOPredicate.CPOPredicate

width-overflow(exp, ikind): the value of the expression fits in an integer of ikind.

  • tags[1]: ikind

  • args[0]: exp

property exp: CExp
has_variable(vid: int) → bool[source]

Return true if the variable with vid occurs in any subexpression.

property ikind: str
property is_width_overflow: bool
chc.proof.CPOPredicate.get_predicate_name(tag: str) → str[source]
chc.proof.CPOPredicate.get_predicate_tag(name: str) → str[source]