Skip to content
Small C projects as demonstration targets for the CodeHawk-C Analyzer
Branch: master
Clone or download

Latest commit

Fetching latest commit…
Cannot retrieve the latest commit at this time.

Files

Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
targets
.gitignore
LICENSE
README.md

README.md

CodeHawk-C-Targets-Misc

Small C projects as demonstration targets for the CodeHawk-C Analyzer

Description

This repository contains small C applications that have been pre-parsed (on linux) and are ready for analysis with the CodeHawk C Analyzer. The reason to provide a pre-parsed version of the application is that all analyses will be comparable. Local configuration and versions of standard library header files may affect the proof obligations generated and thus result in different analysis results for different computers.

Access from the CodeHawk-C analyzer

Add the following line to your chc/util/ConfigLocal.py file (if not present, copy from chc/util/ConfigLocal.template):

    misctargets_home = os.path.expanduser('~')
    config.targets = {
        "misc": os.path.join(misctargets_home,'CodeHawk-C-Targets-Misc/targets/misc.json')
        }

(modify misctargets_home to hold your local path to the CodeHawk-C-Targets-Misc directory, if necessary). When registered in this way the path to the project can be specified with misc: followed by the name of the project, e.g., misc:file, in every script in the chc/cmdline/c-project directory. For example, to analyze the file project listed below:

> export PYTHONPATH=$HOME/CodeHawk-C
> python chc_analyze_project.py misc:file --verbose

and to view the results when analysis is completed

> python chc_report_project.py misc:file

Applications

file

  • description: an older version of the linux file utility https://github.com/file/file
  • size: 20 .c files, 287 functions, 14,966 LOC
  • semantic size: 7637 statements, 1860 calls, 2852 assignments (more detailed statistics)
  • primary proof obligations (ppo's): 54,477
  • current analysis status: 46,425 ppo's proven safe or delegated (85.2%), 8052 ppo's not yet proven (14.8%) (more detailed results, broken down by file and proof obligation kind)
  • contract conditions: no preconditions, 190 postconditions
  • analysis time: approximately 20 mins (single core), or 9 mins (4 cores), or 5 mins (10 cores).

hping

  • desciption: hping is a command-line oriented TCP/IP packet assembler analyzer available from GitHub. The version used in this repository is an older version.
  • size: 55 .c files, 337 functions, 13,224 LOC
  • semantic size: 5213 statements, 1916 calls, 2173 assignments
  • primary proof obligations (ppo's): 43,526
  • current analysis status> 35,579 ppo's proven safe or delegated (81.7%), 7948 ppo's not yet proven (18.3%) (more detailed results, broken down by file and proof obligation kind)
  • contract conditions: 111 preconditions, 81 postconditions
  • analysis time: approximately 5 mins (4 cores)
You can’t perform that action at this time.