chc.proof.CFunctionReturnsiteSPOs module

All supporting proof obligations associated with a single return site.

class chc.proof.CFunctionReturnsiteSPOs.CFunctionReturnsiteSPOs(cproofs: CFunctionProofs, xnode: xml.etree.ElementTree.Element)[source]

Bases: object

Represents the supporting proof obligations associated with a return site.

All return site supporting proof obligations are generated by the analyzer.

property cfgcontext: CfgContext

property cfile: CFile

property cfun: CFunction

property context: ProgramContext

property contextdictionary: CContextDictionary

property cproofs: CFunctionProofs

get_spo(id: int) → chc.proof.CFunctionReturnsiteSPO.CFunctionReturnsiteSPO[source]

has_spo(id: int) → bool[source]

iter(f: Callable[[chc.proof.CFunctionReturnsiteSPO.CFunctionReturnsiteSPO], None]) → None[source]

property line: int

property location: chc.app.CLocation.CLocation

property podictionary: CFunPODictionary

property spos: Dict[int, List[chc.proof.CFunctionReturnsiteSPO.CFunctionReturnsiteSPO]]

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