chc.proof.PPOType module

Base class and subclasses:

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

Base class for primary proof obligation types.

chc.proof.PPOType.ProgramPPOType(pod, ixval)

Primary proof obligation generated for constructs that may lead to UB.

chc.proof.PPOType.LibPPOType(pod, ixval)

Primary proof obligation generated for library calls that may lead to UB.

Primary proof obligation as generated.

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

Bases: chc.proof.PPOType.PPOType

Primary proof obligation generated for library calls that may lead to UB.

  • tags[1]: name of library function called

  • 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 is_lib_ppo: bool
property lib_function_name: str
property location: CLocation
property precondition: XPredicate
property predicate: CPOPredicate
class chc.proof.PPOType.PPOType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.CFunPODictionaryRecord.CFunPOType

Base class for primary proof obligation types.

property is_lib_ppo: bool
property is_program_ppo: bool
class chc.proof.PPOType.ProgramPPOType(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.proof.PPOType.PPOType

Primary proof obligation generated for constructs that may lead to UB.

  • 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_program_ppo: bool
property location: CLocation
property predicate: CPOPredicate