chc.proof.CFunctionSPOs module

Container for all supporting proof obligations in a function.

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

Bases: object

Represents the set of supporting proof obligations for a function.

xnode received is the content of the <”spos”> element.

property callsite_spos: Dict[str, chc.proof.CFunctionCallsiteSPOs.CFunctionCallsiteSPOs]

property cfun: CFunction

collect_post_assumes() → None[source]: for all call sites collect postconditions from callee’s contracts and add as assume.

property cproofs: CFunctionProofs

distribute_post_guarantees() → None[source]

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

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

iter_callsites(f: Callable[[chc.proof.CFunctionCallsiteSPOs.CFunctionCallsiteSPOs], None]) → None[source]

property local_spos: Dict[int, chc.proof.CFunctionLocalSPO.CFunctionLocalSPO]

property podictionary: CFunPODictionary

property returnsite_spos: Dict[str, chc.proof.CFunctionReturnsiteSPOs.CFunctionReturnsiteSPOs]

property spos: List[chc.proof.CFunctionPO.CFunctionPO]

update() → None[source]

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