chc.app.CFile module

C-file main access point.

class chc.app.CFile.CFile(capp: CApplication, index: int, cfilename: str, cfilepath: Optional[str])

Bases: object

C File main access point.

property assigndictionary: chc.app.CFileAssignmentDictionary.CFileAssignmentDictionary

property capp: CApplication

property cfileglobals: chc.app.CFileGlobals.CFileGlobals

property cfilename: str

Returns base filename (without extension).

property cfilepath: Optional[str]

Returns path relative to project directory or None if at toplevel.

collect_post_assumes() → None

Collect callsite postconditions from callee’s contracts and add as assume.

property contextdictionary: chc.app.CContextDictionary.CContextDictionary

property contractpath: str

property contracts: chc.api.CFileContracts.CFileContracts

create_contract(contractpath, preservesmemory=[], seed={}, ignorefns={})

property declarations: chc.app.CFileDeclarations.CFileDeclarations

property dictionary: chc.app.CFileDictionary.CFileDictionary

property functioncount: int

property functionnames: List[str]

property functions: Dict[int, chc.app.CFunction.CFunction]

property functionxref: Dict[str, int]

Returns a map from function names to vid’s.

property gcomptagdecls: Dict[int, chc.app.CFileGlobals.CGCompTag]

property gcomptagdefs: Dict[int, chc.app.CFileGlobals.CGCompTag]

property genumtagdecls: Dict[str, chc.app.CFileGlobals.CGEnumTag]

property genumtagdefs: Dict[str, chc.app.CFileGlobals.CGEnumTag]

get_callinstrs() → List[CCallInstr]

get_compinfo_by_ckey(ckey: int) → CCompInfo

get_compinfos() → List[CCompInfo]

get_fn_spos(fname: str) → List[chc.proof.CFunctionPO.CFunctionPO]

get_function_by_index(index: int) → chc.app.CFunction.CFunction

get_function_by_name(fnname: str) → chc.app.CFunction.CFunction

get_function_contract(name: str) → Optional[chc.api.CFunctionContract.CFunctionContract]

get_functions() → Iterable[chc.app.CFunction.CFunction]

get_global_varinfo(vid: int) → CVarInfo

get_global_varinfo_by_name(name: str) → CVarInfo

get_line_ppos() → Dict[int, Dict[str, Any]]

get_max_functionname_length() → int

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

Returns a list of open primary proof obligations.

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

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

Returns a list of primary proof obligations delegated.

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

Returns a list of primary proof obligations violated.

get_source_line(n: int) → str

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

get_strings() → Dict[str, List[str]]

Returns a list of the strings referenced in this file.

get_variable_uses(vid: int) → Dict[str, int]

Returns a mapping from function name to a count of variable refs.

function name -> number of references with a given vid.

property gfunctions: Dict[int, chc.app.CFileGlobals.CGFunction]

property gtypes: Dict[str, chc.app.CFileGlobals.CGType]

property gvardecls: Dict[int, chc.app.CFileGlobals.CGVarDecl]

property gvardefs: Dict[int, chc.app.CFileGlobals.CGVarDef]

has_file_contracts() → bool

has_function_by_index(index: int) → bool

has_function_by_name(fnname: str) → bool

has_function_contract(name: str) → bool

has_global_varinfo(vid: int) → bool

has_global_varinfo_by_name(name: str) → bool

has_outstanding_fn_api_requests() → bool

Returns true if any of this file’s functions posted a request.

property index: int

property interfacedictionary: chc.api.InterfaceDictionary.InterfaceDictionary

iter_functions(f: Callable[[chc.app.CFunction.CFunction], None]) → None

property name: str

Returns the full name relative to the project directory.

Note: the filename is without extension

property predicatedictionary: chc.proof.CFilePredicateDictionary.CFilePredicateDictionary

property projectname: str

reinitialize_tables() → None

reload_ppos() → None

reload_spos() → None

reset_contextdictionary() → None

reset_declarations() → None

reset_dictionary() → None

reset_interfacedictionary() → None

reset_predicatedictionary() → None

save_declarations() → None

save_interface_dictionary() → None

save_predicate_dictionary() → None

save_user_assumptions(userdata, assumptions)

property sourcefile: chc.source.CSrcFile.CSrcFile

property targetpath: str

exception chc.app.CFile.CFunctionNotFoundException(cfile: chc.app.CFile.CFile, functionname: str)

Bases: Exception