chc.proof.CFunctionProofs module

Main access point for a function’s primary and supporting proof obligations.

class chc.proof.CFunctionProofs.CFunctionProofs(cfun: CFunction, xpponode: xml.etree.ElementTree.Element, xsponode: xml.etree.ElementTree.Element)[source]

Bases: object

CFunctionProofs is the root of a data structure that provides access to all proof obligations and associated evidence. Relationships between proof obligation and evidence are established through the CFunctionProofs object.

  • CFunctionProofs

    • ppos: CFunctionPPOs

    • id -> CFunctionPPO

    • spos: CFunctionSPOs

    • callsitespos: context -> CFunctionCallsiteSPOs

    • id -> CFunctionCallsiteSPO

    • returnsitespos: context -> CFunctionReturnsiteSPOs

    • id -> CFunctionReturnsiteSPO

property capp: CApplication
property cfile: CFile
property cfilename: str
property cfilepath: Optional[str]
property cfun: CFunction
collect_post_assumes() → None[source]

For all call sites collect postconditions from callee’s contracts and add as assume.

distribute_post_guarantees() → None[source]
get_open_spos() → List[chc.proof.CFunctionPO.CFunctionPO][source]
get_ppo(id: int) → chc.proof.CFunctionPPO.CFunctionPPO[source]
get_spo(id: int) → chc.proof.CFunctionPO.CFunctionPO[source]
get_spo_violations() → List[chc.proof.CFunctionPO.CFunctionPO][source]
get_spos() → List[chc.proof.CFunctionPO.CFunctionPO][source]
iter_callsites(f: Callable[[chc.proof.CFunctionCallsiteSPOs.CFunctionCallsiteSPOs], None]) → None[source]
iter_ppos(f: Callable[[chc.proof.CFunctionPPO.CFunctionPPO], None]) → None[source]
iter_spos(f: Callable[[chc.proof.CFunctionPO.CFunctionPO], None]) → None[source]
property open_ppos: List[chc.proof.CFunctionPO.CFunctionPO]
property open_spos: List[chc.proof.CFunctionPO.CFunctionPO]
property ppolist: List[chc.proof.CFunctionPO.CFunctionPO]
property ppos: chc.proof.CFunctionPPOs.CFunctionPPOs
property ppos_delegated: List[chc.proof.CFunctionPO.CFunctionPO]
property ppos_violated: List[chc.proof.CFunctionPO.CFunctionPO]
property projectname: str
reload_ppos() → None[source]
reload_spos() → None[source]
reset_ppos() → None[source]
reset_spos() → None[source]
save_spos() → None[source]
property spo_violations: List[chc.proof.CFunctionPO.CFunctionPO]
property spolist: List[chc.proof.CFunctionPO.CFunctionPO]
property spos: chc.proof.CFunctionSPOs.CFunctionSPOs
property targetpath: str
update_spos() → None[source]