chc.proof.CFunPODictionaryRecord module

Base class for objects in the function-level proof obligation dictionary.

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

Bases: chc.util.IndexedTable.IndexedTableValue

property capp: CApplication

property cdecls: CFileDeclarations

property cfile: CFile

property cfun: CFunction

property cxd: CContextDictionary

property ifd: InterfaceDictionary

property pd: CFilePredicateDictionary

property pod: CFunPODictionary

class chc.proof.CFunPODictionaryRecord.CFunPODictionaryRegistry[source]

Bases: object

mk_instance(pod: CFunPODictionary, ixval: chc.util.IndexedTable.IndexedTableValue, anchor: Type[chc.proof.CFunPODictionaryRecord.PodR]) → chc.proof.CFunPODictionaryRecord.PodR[source]

register_tag(tag: str, anchor: type) → Callable[[type], type][source]

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

Bases: chc.proof.CFunPODictionaryRecord.CFunPODictionaryRecord

property context: ProgramContext

property external_id: int

property location: CLocation

property po_index: int

property predicate: CPOPredicate