chc.proof.SPOType module

Base class and subclasses:

chc.proof.SPOType.SPOType(pod, ixval)

Base class for supporting proof obligation types.

chc.proof.SPOType.LocalSPOType(pod, ixval)

Proof obligation that supports an assumption within a function.

chc.proof.SPOType.CallsiteSPOType(pod, ixval)

Proof obligation that supports an assumption on a function call argument.

chc.proof.SPOType.ReturnsiteSPOType(pod, ixval)

Proof obligation that supports an assumption on a return value.

Supporting proof obligation as generated to provide evidence for assumptions.

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

Bases: chc.proof.SPOType.SPOType

Proof obligation that supports an assumption on a function call argument.

  • args[0]: index of location in cdeclarations

  • args[1]: index of context in contexts

  • args[2]: index of predicate in predicate dictionary

  • args[3]: api-id

property context: ProgramContext
property external_id: int
property is_callsite_spo: bool
property location: CLocation
property predicate: CPOPredicate
class chc.proof.SPOType.LocalSPOType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.SPOType.SPOType

Proof obligation that supports an assumption within a function.

  • args[0]: index of location in cdeclarations

  • args[1]: index of context in contexts

  • args[2]: index of predicate in predicate dictionary

property context: ProgramContext
property is_local_spo: bool
property location: CLocation
property predicate: CPOPredicate
class chc.proof.SPOType.ReturnsiteSPOType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.SPOType.SPOType

Proof obligation that supports an assumption on a return value.

  • args[0]: index of location in cdeclarations

  • args[1]: index of context in contexts

  • args[2]: index of predicate in predicate dictionary

  • args[3]: index of xpredicate in interface dictionary

property context: ProgramContext
property external_id: int
property is_returnsite_spo: bool
property location: CLocation
property postcondition: XPredicate
property predicate: CPOPredicate
class chc.proof.SPOType.SPOType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CFunPODictionaryRecord.CFunPOType

Base class for supporting proof obligation types.

property external_id: int
property is_callsite_spo: bool
property is_local_spo: bool
property is_returnsite_spo: bool