chc.app.CApplication module

Main access point to the analysis of a C application.

class chc.app.CApplication.CApplication(projectpath: str, projectname: str, targetpath: str, contractpath: str, singlefile: bool = False, excludefiles: List[str] = [])

Bases: object

Primary access point for source code and analysis results.

An application can consist of a single file, or of multiple files managed by a Makefile.

In case of a single file the following call on CApplication initializes the single file:

• capp.initialize_single_file(cfilename)

The filepath in this case is assumed to be empty. The file index is set to 0.

In case of multiple files the following file is assumed to be present in the top analysis-results directory:

• <projectpath>/<projectname>.cch/a/target_files.xml

This file, normally created by the CodeHawk-C parser, is expected to contain a list of c-file entries that provide the attributes:

• id: a unique file index, a number greater than zero;

• name: a string denoting the relative path of the file w.r.t. the project directory (e.g., src/cgi/buffer.c)

property callgraph: Dict[Tuple[int, int], List[Tuple[Tuple[int, int], CFunctionCallsiteSPOs]]]

property cfiles: Iterable[chc.app.CFile.CFile]

collect_post_assumes() → None

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

property contractpath: str

convert_vid(filevar: chc.app.IndexManager.FileVarReference, tgtfid: int) → int

property declarations: chc.app.CGlobalDeclarations.CGlobalDeclarations

property dictionary: chc.app.CGlobalDictionary.CGlobalDictionary

distribute_post_guarantees() → None

add callee postcondition guarantees to call sites as assumptions

property excludefiles: List[str]

property filenames: List[str]

Returns full filenames relative to the project path (without .c).

property files: Dict[int, chc.app.CFile.CFile]

Returns a map from file-indexes to CFile objects.

property filexref: Dict[str, int]

Returns a map from c filenames to file-indexes.

Note: filenames include extension and paths relative to project directory.

get_callinstrs() → List[CCallInstr]

get_callsites(fid: int, vid: int) → List[Tuple[Tuple[int, int], CFunctionCallsiteSPOs]]

Return a list of ((fid, vid), callsitespos).

get_cfile() → chc.app.CFile.CFile

Returns the CFile object in a single-file project.

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

get_file(fname: str) → chc.app.CFile.CFile

Access to file with full relative path and no extension.

get_file_by_index(index: int) → chc.app.CFile.CFile

get_function(filevar: chc.app.IndexManager.FileVarReference) → CFunction

get_function_by_index(index: int) → CFunction

get_gckey(filekey: chc.app.IndexManager.FileKeyReference) → Optional[int]

get_line_counts() → str

get_max_filename_length() → int

get_open_ppos() → List[CFunctionPO]

get_ppos() → List[CFunctionPO]

get_ppos_delegated() → List[CFunctionPO]

get_ppos_violated() → List[CFunctionPO]

get_project_counts(filefilter: Callable[[str], bool] = <function CApplication.<lambda>>) → Tuple[int, int, int]

get_spos() → List[CFunctionPO]

property globalcontract: chc.api.CGlobalContract.CGlobalContract

has_file(fname: str) → bool

has_file_index(index: int) → bool

has_function(filevar: chc.app.IndexManager.FileVarReference) → bool

property indexmanager: chc.app.IndexManager.IndexManager

initialize_files(filenames: Dict[int, str]) → None

initialize_single_file(fname: str) → None

is_application_header(name: str) → bool

Returns true if the name corresponds to an application file.

property is_singlefile: bool

iter_files(f: Callable[[chc.app.CFile.CFile], None]) → None

iter_files_parallel(f: Callable[[chc.app.CFile.CFile], None], processes: int) → None

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

iter_functions_parallel(f: Callable[[CFunction], None], maxprocesses: int) → None

property projectname: str

property projectpath: str

reinitialize_tables() → None

reload_ppos() → None

Reload primary proof obligations after analyzer has run.

reload_spos() → None

Reload supporting proof obligations after analyzer has run.

resolve_vid_function(filevar: chc.app.IndexManager.FileVarReference) → Optional[CFunction]

Returns the function def for the local file-index fid and vid.

Note: the function definition may or may not reside in the same file, that is, the c-file with index fid may have a function declaration for the function with index vid, but not a a definition.

The location of the definition is obtained from the index manager via the corresponding global index of the (local) vid (as initialized by the linker).

property revcallgraph: Dict[Tuple[int, int], List[Tuple[Tuple[int, int], CFunctionCallsiteSPOs]]]

property targetpath: str

update_spos() → None

Create supporting proof obligations for all call sites.