chc.app.CFunction module

Main access point for a c function.

class chc.app.CFunction.CFunction(cfile: CFile, xnode: xml.etree.ElementTree.Element, fname: str)[source]

Bases: object

Function implementation.

property api: chc.api.CFunctionApi.CFunctionApi

property block_count: int

property call_instrs: List[chc.app.CInstr.CCallInstr]

property capp: CApplication

property cfile: CFile

property cfiledecls: CFileDeclarations

property cfilename: str

property cfilepath: Optional[str]

property cfundecls: chc.app.CFunDeclarations.CFunDeclarations

collect_post() → None[source]: Add postcondition requests to the contract of the callee

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

distribute_post_guarantees() → None[source]

property formals: Dict[int, CVarInfo]

property ftype: CTyp

get_api() → chc.api.CFunctionApi.CFunctionApi[source]

get_contract_condition_violations() → List[Tuple[str, str]][source]

get_formal_vid(name: str) → int[source]

get_formals() → List[CVarInfo][source]

get_function_contract() → Optional[CFunctionContract][source]

get_line_number() → int[source]

get_locals() → List[CVarInfo][source]

get_location() → chc.app.CLocation.CLocation[source]

get_open_ppos() → List[chc.proof.CFunctionPO.CFunctionPO][source]

get_open_spos() → List[chc.proof.CFunctionPO.CFunctionPO][source]

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

get_ppos() → List[chc.proof.CFunctionPO.CFunctionPO][source]

get_ppos_delegated() → List[chc.proof.CFunctionPO.CFunctionPO][source]

get_ppos_violated() → List[chc.proof.CFunctionPO.CFunctionPO][source]

get_source_code_file() → str[source]

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

get_spo_violations() → List[chc.proof.CFunctionPO.CFunctionPO][source]

get_spos() → List[chc.proof.CFunctionPO.CFunctionPO][source]

get_variable_uses(vid: int) → int[source]

get_variable_vid(vname: str) → int[source]

get_vid() → int[source]

has_function_contract() → bool[source]

has_line_number() → bool[source]

has_location() → bool[source]

has_outstanding_api_requests() → bool[source]

has_source_code_file() → bool[source]

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

property instr_count: int

property interfacedictionary: InterfaceDictionary

property invarianttable: chc.invariants.CFunInvariantTable.CFunInvariantTable

property invdictionary: chc.invariants.CFunInvDictionary.CFunInvDictionary

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

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

property locals: Dict[int, CVarInfo]

property name: str

property podictionary: chc.proof.CFunPODictionary.CFunPODictionary

property projectname: str

property proofs: chc.proof.CFunctionProofs.CFunctionProofs

reinitialize_tables() → None[source]

reload_ppos() → None[source]

reload_spos() → None[source]

save_pod() → None[source]

save_spos() → None[source]

property sbody: chc.app.CStmt.CFunctionBody

selfignore()[source]

property stmt_count: int

property strings: List[str]

property svar: CVarInfo

property targetpath: str

update_spos() → None[source]

property vardictionary: chc.invariants.CFunVarDictionary.CFunVarDictionary

violates_contract_conditions() → bool[source]

xmsg(txt: str) → str[source]