chc.cmdline.c_file.cfileutil module

Implementation of commands for processing single files in the CLI.

The functions in this module support the commands available in the single-file mode of the CodeHawk-C analyzer.

Naming conventions used in this module:

  • pcfilename_c full-path name of cfile analyzed

  • cfilename base name of cfile analyzed (without extension)

  • cfilename_c idem, with .c extension

  • projectpath full-path of directory in which cfilename_c resides

  • targetpath full-path of directory in which results are saved

  • projectname name under which results are saved

Unless specified otherwise the following defaults are used:

  • targetpath : set equal to projectpath

  • projectname: set to cfilename

The results are stored in the directory

targetpath/projectname.cch

chc.cmdline.c_file.cfileutil.cfile_analyze_file(args: argparse.Namespace) → NoReturn[source]

Analyzes a single c-file and saves the results in the .cch directory.

This command runs the ocaml C analyzer to

  1. generate proof obligations for the declarations and functions represented by the data structures saved by the parse command,

  2. generate invariants for these functions (targeted for the proof obligations),

  3. attempts to discharge the generated proof obligations with the generated invariants

  4. generates supporting proof obligations for proof obligations that were discharged against an api assumption (on the python side)

  5. repeats steps 2-4 until convergence (or some preset maximum is reached)

All results are saved in the <projectname>.cch/a/ directory

chc.cmdline.c_file.cfileutil.cfile_investigate_file(args: argparse.Namespace) → NoReturn[source]

Shows a list of open, delegated, and violated proof obligations.

The proof obligations are presented grouped by proof obliigation type and function. The proof obligation types can be optionally restricted by listing the proof obliigations of interest (e.g., not-null) explicitly.

chc.cmdline.c_file.cfileutil.cfile_parse_file(args: argparse.Namespace) → NoReturn[source]

Parses a single file and saves the results in the .cch directory.

This command runs the gcc preprocessor on the single c-file presented and then calls the ocaml C analyzer to parse (using the goblint cil parser) the resulting .i file into ocaml data structures. These data structures are saved in the <projectname>.cch/a directory. The original c-file and the preprocessed i-file are saved in the <projectname>.cch/s directory.

Note: When run on a MacOSX platform, the CIL parser may not be able to handle the syntax of the MacOS standard header files, if these are included in the c-file.

chc.cmdline.c_file.cfileutil.cfile_report_file(args: argparse.Namespace) → NoReturn[source]

Reports the analysis results for a single file.

This command loads the analysis results saved by the analysis command and prints the result statistics (in terms of proof obligations discharged), and optionally prints the indivual proof obligations embedded in the original source code (if available from the <projectname>.cch/s/ directory).

chc.cmdline.c_file.cfileutil.cfile_showglobals(args: argparse.Namespace) → NoReturn[source]

Shows the global definitions and declarations in a c-file.

chc.cmdline.c_file.cfileutil.cfile_testlibc_summary(args: argparse.Namespace) → NoReturn[source]

Runs one of the programs in tests/libcsummaries

A combination of a header file and a function name from that header may have a test program associated with it (see tests/testfiles.json).

chc.cmdline.c_file.cfileutil.print_error(m: str) → None[source]
chc.cmdline.c_file.cfileutil.set_logging(level: str, path: str, logfilename: Optional[str], msg: str = '', mode: str = 'a') → None[source]