chc.proof.CFunPODictionary module

Dictionary of proof obligation types at function level.

class chc.proof.CFunPODictionary.CFunPODictionary(cfun: CFunction, xnode: xml.etree.ElementTree.Element)[source]

Bases: object

Indexed function proof obligations.

property capp: CApplication

property cfile: CFile

property cfun: CFunction

get_assumption_type(ix: int) → chc.proof.AssumptionType.AssumptionType[source]

get_assumption_type_map() → Dict[int, chc.util.IndexedTable.IndexedTableValue][source]

get_ppo_type(ix: int) → chc.proof.PPOType.PPOType[source]

get_ppo_type_map() → Dict[int, chc.util.IndexedTable.IndexedTableValue][source]

get_spo_type(ix: int) → chc.proof.SPOType.SPOType[source]

get_spo_type_map() → Dict[int, chc.util.IndexedTable.IndexedTableValue][source]

index_assumption_type(tags: List[str], args: List[int]) → int[source]

index_ppo_type(tags: List[str], args: List[int]) → int[source]

index_spo_type(tags: List[str], args: List[int]) → int[source]

initialize(xnode: xml.etree.ElementTree.Element) → None[source]

property interfacedictionary: InterfaceDictionary

objectmap_to_string(name: str) → str[source]

property pd: CFilePredicateDictionary

read_xml_assumption_type(txnode: xml.etree.ElementTree.Element, tag: str = 'iast') → chc.proof.AssumptionType.AssumptionType[source]

read_xml_ppo_type(txnode: xml.etree.ElementTree.Element, tag: str = 'ippo') → chc.proof.PPOType.PPOType[source]

read_xml_spo_type(txnode: xml.etree.ElementTree.Element, tag: str = 'ispo') → chc.proof.SPOType.SPOType[source]

write_xml(node: xml.etree.ElementTree.Element) → None[source]

write_xml_spo_type(txnode: xml.etree.ElementTree.Element, spotype: chc.proof.SPOType.SPOType, tag: str = 'ispo') → None[source]