chc.cmdline.chkc module

Command-line interface to the CodeHawk C Analyzer.

The CodeHawk C Analyzer is a sound static analysis tool that attempts to prove the absence of undefined behavior. It does so by generating a comprehensive set of proof obligations that capture all conditions that can lead to undefined behavior and attempts to prove that the negation of those conditions is valid, that is true for all inputs. The status of these proof obligations can then be inspected via various reports.

The CodeHawk-C analyzer calls two executables from the codehawk repository that perform the parsing and analysis. To check if these two executables are available, you can run:

• chkc info

Analysis commands are provided for two distinct ways of analysis:

• chkc c-file …. analyzes a single source file (that can be parsed by gcc)

• chkc c-project …

  analyzes a project of multiple files that comes with a Makefile

Run the respective option for more information on either one.

chc.cmdline.chkc.cfile_filetable_command(args: argparse.Namespace) → NoReturn

chc.cmdline.chkc.cfile_functiontable_command(args: argparse.Namespace) → NoReturn

chc.cmdline.chkc.cfilecommand(args: argparse.Namespace) → NoReturn

chc.cmdline.chkc.cprojectcommand(args: argparse.Namespace) → NoReturn

chc.cmdline.chkc.julietcommand(args: argparse.Namespace) → NoReturn

chc.cmdline.chkc.parse() → argparse.Namespace

chc.cmdline.chkc.showinfo(args: argparse.Namespace) → NoReturn

chc.cmdline.chkc.showversion(args: argparse.Namespace) → NoReturn