chc.proof.CFunctionPPOs module

The collection of all primary proof obligations in a function.

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

Bases: object

Represents the set of primary proof obligations for a function.

xnode received is the content of the <”ppos”> element

property cfile: CFile

property cfun: CFunction

property contextdictionary: CContextDictionary

property cproofs: CFunctionProofs

get_ppo(id: int) → chc.proof.CFunctionPPO.CFunctionPPO[source]

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

property podictionary: CFunPODictionary

property ppos: Dict[int, chc.proof.CFunctionPPO.CFunctionPPO]