chc.api.InterfaceDictionary module

Dictionary of all non-local symbolic values.

class chc.api.InterfaceDictionary.InterfaceDictionary(cfile: CFile, xnode: Optional[xml.etree.ElementTree.Element])[source]

Bases: object

Function interface constructs.

Parameters

cfile (CFile) – c-file that owns the dictionary
xnode (Optional[ET.Element]) – xml element that holds the entries in the dictionary

property cfile: CFile

property declarations: CFileDeclarations

property dictionary: CFileDictionary

get_api_parameter(ix: int) → chc.api.ApiParameter.ApiParameter[source]

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

get_opt_s_term(ix: int) → Optional[chc.api.STerm.STerm][source]

get_postassume(ix: int) → chc.api.PostAssume.PostAssume[source]

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

get_postrequest(ix: int) → chc.api.PostRequest.PostRequest[source]

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

get_s_offset(ix: int) → chc.api.SOffset.SOffset[source]

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

get_s_term(ix: int) → chc.api.STerm.STerm[source]

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

get_xpredicate(ix: int) → chc.api.XPredicate.XPredicate[source]

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

index_api_parameter(p: chc.api.ApiParameter.ApiParameter) → int[source]

index_opt_s_term(t: Optional[chc.api.STerm.STerm]) → int[source]

index_s_offset(t: chc.api.SOffset.SOffset) → int[source]

index_s_term(t: chc.api.STerm.STerm) → int[source]

index_xpredicate(p: chc.api.XPredicate.XPredicate) → int[source]

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

mk_arg_no_offset() → chc.api.SOffset.SOffset[source]

mk_field_s_term(fieldname: str) → chc.api.STerm.STerm[source]

mk_formal_api_parameter(n: int) → chc.api.ApiParameter.ApiParameter[source]

mk_global_api_parameter(g: str) → chc.api.ApiParameter.ApiParameter[source]

mk_initialized_xpredicate(t: chc.api.STerm.STerm) → chc.api.XPredicate.XPredicate[source]

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

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

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

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

parse_mathml_api_parameter(name: str, pars: Dict[str, int], gvars: List[str] = []) → int[source]

parse_mathml_offset(tnode: Optional[xml.etree.ElementTree.Element]) → int[source]

parse_mathml_term(tnode: xml.etree.ElementTree.Element, pars: Dict[str, int], gvars: List[str] = []) → int[source]

parse_mathml_xpredicate(pcnode: xml.etree.ElementTree.Element, pars: Dict[str, int], gvars: List[str] = []) → int[source]

read_xml_postcondition(node: xml.etree.ElementTree.Element, tag: str = 'ixpre') → chc.api.XPredicate.XPredicate[source]

read_xml_postrequest(node: xml.etree.ElementTree.Element, tag: str = 'iipr') → chc.api.PostRequest.PostRequest[source]

read_xml_xpredicate(node: xml.etree.ElementTree.Element, tag: str = 'ipr') → chc.api.XPredicate.XPredicate[source]

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

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

write_xml_postcondition(node: xml.etree.ElementTree.Element, pc: chc.api.XPredicate.XPredicate, tag: str = 'ixpre') → None[source]