CONTRACT Artifact

CONTRACT is a specification-driven static analysis workflow for C/C++ projects.

Technical Pipeline

Step 0: Cleanup temporary files and validate compile_commands.json
    │
    ▼
Step 1: Extract function prototypes and build call graph
        (LLVM16 plugin: ExtractFunctionPrototypes.so)
    │
    ▼
Step 2: Parse call graph and generate specifications
        (LLVM16 plugin: spec_gen.so)
    │
    ▼
Step 3: Run specification-based checker via CodeChecker
        (LLVM17 plugin: StringBasedChecker.so)
    │
    ▼
Output: HTML bug report

How to Run

config the path in config.py and config.yaml for the llvm and the API key first.

cd contract
python run.py --project_dir /path/to/target/project 

The target project must contain compile_commands.json, which use clang-17.

make clean 
export CC=clang
export CXX=clang++
export HOSTCC=clang
CodeChecker log -b "make CC=clang HOSTCC=clang -j$(nproc)" -o compile_commands.json

Repository Structure

contract/           Core Python scripts (run.py is the entry point)
plugin_src/
  llvm16/
    ExtractFunction/    Function prototype extraction plugin
    SpecGeneration/     Specification generation plugin
  llvm17/
    SpecDetection/      Specification-based checker plugin