chc.proof.CFunctionReturnsiteSPO module

Supporting proof obligation for a return site.

class chc.proof.CFunctionReturnsiteSPO.CFunctionReturnsiteSPO(crspos: CFunctionReturnsiteSPOs, potype: CFunPOType, status: str = 'open', deps: Optional[CProofDependencies] = None, expl: Optional[str] = None, diag: Optional[CProofDiagnostic] = None)[source]

Bases: chc.proof.CFunctionPO.CFunctionPO

Represents a secondary proof obligation associated with a return site.

property crspos: CFunctionReturnsiteSPOs
property external_id: int
write_xml(cnode: xml.etree.ElementTree.Element) → None[source]