chc.cmdline.AnalysisManager module

class chc.cmdline.AnalysisManager.AnalysisManager(capp: CApplication, wordsize: int = 0, unreachability: bool = False, thirdpartysummaries: List[str] = [], nofilter: bool = True, verbose: bool = False)

Bases: object

Provide the interface to the codehawk (ocaml) analyzer.

property canalyzer: str

property capp: CApplication

property chsummaries: str

property config: chc.util.Config.Config

property contractpath: Optional[str]

create_app_primary_proofobligations(processes: int = 1) → None

Call analyzer to create ppo’s for all application files.

create_file_primary_proofobligations(cfilename: str, cfilepath: Optional[str] = None) → None

Call analyzer to create primary proof obligations for a single file.

generate_and_check_app(domains: str, processes: int = 1) → None

Generate invariants and check proof obligations for application.

generate_and_check_file(cfilename: str, cfilepath: Optional[str], domains: str) → None

Generate invariants and check proof obligations for a single file.

property projectname: str

property projectpath: str

reset() → None

Remove all file- and function-level files produced by the analysis.

reset_logfiles() → None

Remove all log files from semantics directory.

reset_tables(cfile: CFile) → None

Reload dictionaries from file (to get updated data from analyzer).

property targetpath: str