chc.proof.AssumptionType module

Base class and subclasses

`chc.proof.AssumptionType.AssumptionType`(pod, ...)	Base class for assumption types.
`chc.proof.AssumptionType.ApiAssumptionType`(...)	Assumption on parameters of the function.
`chc.proof.AssumptionType.GlobalApiAssumptionType`(...)	Assumption on global variable values upon entry of the function.
`chc.proof.AssumptionType.PostconditionType`(...)	Assumption on the post-condition of a function called.
`chc.proof.AssumptionType.GlobalAssumptionType`(...)	Assumption that is asserted globally that is supported globally.

External assumption on a function.

class chc.proof.AssumptionType.ApiAssumptionType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.AssumptionType.AssumptionType

Assumption on parameters of the function.

This type of assumption gives rise to the corresponding supporting proof obligations on the arguments in the caller of the function.

The index of the predicate is also used as the api-id for the assumption.

args[0]: index of predicate in predicate dictionary

property api_id: int

property is_api_assumption: bool

property predicate: CPOPredicate

class chc.proof.AssumptionType.AssumptionType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CFunPODictionaryRecord.CFunPODictionaryRecord

Base class for assumption types.

property is_api_assumption: bool

property is_contract_assumption: bool

property is_global_api_assumption: bool

property is_global_assumption: bool

property is_local_assumption: bool

class chc.proof.AssumptionType.GlobalApiAssumptionType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.AssumptionType.AssumptionType

Assumption on global variable values upon entry of the function.

Global variables referenced/modified in a function can be viewed as ‘ghost’ parameters to a function, where the function may make some assumption about their value upon function start, but then is responsible for tracking its value locally (assuming no concurrency, or a form of ownership of the global variable throughout function execution.

args[0]: index of predicate in predicate dictionary

property is_global_api_assumption: bool

property predicate: CPOPredicate

class chc.proof.AssumptionType.GlobalAssumptionType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.AssumptionType.AssumptionType

Assumption that is asserted globally that is supported globally.

args[0]: index of xpredicate in interfacedictionary

property is_global_assumption: bool

property xpredicate: XPredicate

class chc.proof.AssumptionType.LocalAssumptionType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.AssumptionType.AssumptionType

Assumption on local variables within a function.

Used in a context where a property can be reduced to local supporting proof obligations. An example is assuming that a call to a function preserves all memory (e.g., does not free any memory).

args[0]: index of predicate in predicate dictionary

property is_local_assumption: bool

property predicate: CPOPredicate

class chc.proof.AssumptionType.PostconditionType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.AssumptionType.AssumptionType

Assumption on the post-condition of a function called.

Note: this assumption type is referred to as a contract assumption, because these types of assumption are usually introduced by means of an externally provided contract.

args[0]: vid of the callee (local file vid)
args[1]: index of xpredicate in interface dictionary

property callee: int

property is_contract_assumption: bool

property xpredicate: XPredicate