chc.proof.CFunctionPO module

Super class of all (primary and supporting) proof obligations.

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

Bases: object

Super class of primary and supporting proof obligations.

property cfg_context: CfgContext

property cfile: CFile

property cfun: CFunction

property context: ProgramContext

property context_strings: str

property cproofs: CFunctionProofs

property dependencies: CProofDependencies

property diagnostic: CProofDiagnostic

property explanation: Optional[str]

get_assumptions() → List[AssumptionType][source]

get_assumptions_type() → str[source]

get_display_prefix() → str[source]

get_global_assumptions() → List[AssumptionType][source]

get_postcondition_assumptions() → List[AssumptionType][source]

get_referral_diagnostics() → Dict[str, List[str]][source]

has_api_dependencies() → bool[source]

has_argument(vid: int) → bool[source]

has_argument_name(vname: str) → bool[source]

has_dependencies() → bool[source]

has_diagnostic() → bool[source]

has_explanation() → bool[source]

has_referral_diagnostic() → bool[source]

has_variable(vid: int) → bool[source]

has_variable_deref(vid: int) → bool[source]

has_variable_name(vname: str) → bool[source]

has_variable_name_deref(vname: str) → bool[source]

has_variable_name_op(vname: str, op: str) → bool[source]

has_variable_op(vid: int, op: str) → bool[source]

property is_closed: bool

property is_deadcode: bool

property is_delegated: bool

property is_implementation_defined: bool

property is_open: bool

property is_ppo: bool

property is_safe: bool

property is_spo: bool

property is_value_wrap_around: bool

property is_violated: bool

property line: int

property location: CLocation

property po_index: int

property pod: CFunPODictionary

property potype: chc.proof.CFunPODictionaryRecord.CFunPOType

property predicate: CPOPredicate

property predicate_name: str

property status: str

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