chc.proof.CFunctionPPO module

Primary proof obligation.

class chc.proof.CFunctionPPO.CFunctionPPO(cproofs: CFunctionProofs, ppotype: CFunPOType, status: str = 'open', deps: Optional[CProofDependencies] = None, expl: Optional[str] = None, diag: Optional[CProofDiagnostic] = None)[source]

Bases: chc.proof.CFunctionPO.CFunctionPO

Represents a primary proof obligation within a function.

is_ppo() → bool[source]